Lean 4 Proof

theorem geometricMeanPeriod_pos {tau_n tau_m : ℝ}
    (hn : 0 < tau_n) (hm : 0 < tau_m) :
    0 < geometricMeanPeriod tau_n tau_m := by
  simp only [geometricMeanPeriod]
  apply mul_pos
  · exact mul_pos (by norm_num) Real.pi_pos
  · exact Real.sqrt_pos_of_pos (mul_pos hn hm)

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:105

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file