pith. machine review for the scientific record. sign in
theorem proved term proof

amati_increases

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  53theorem amati_increases (E₁ E₂ C : ℝ) (hE₁ : 0 < E₁) (hC : 0 < C) (h : E₁ < E₂) :
  54    amati_peak E₁ C < amati_peak E₂ C := by

proof body

Term-mode proof.

  55  unfold amati_peak
  56  apply mul_lt_mul_of_pos_left _ hC
  57  exact Real.rpow_lt_rpow (le_of_lt hE₁) h (by norm_num)
  58
  59/-- Amati exponent 1/2 from Γ ∝ E_iso^(1/4) × √(E_iso) combination. -/

depends on (2)

Lean names referenced from this declaration's body.