Documentation

Lean 4 Proof

theorem criticalMassJ_increasing_in_T {ρ c d_sq T₁ T₂ : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq) (hρ : ρ < 1)
    (hT : T₁ < T₂) :
    criticalMassJ T₁ ρ c d_sq < criticalMassJ T₂ ρ c d_sq := by
  simp only [criticalMassJ]
  apply div_lt_div_of_pos_right
  · exact mul_lt_mul_of_pos_right hT (by linarith)
  · positivity

Dependency Graph

Location

thesis/CESProofs/EntryExit/Defs.lean:97

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file