Documentation

Lean 4 Proof

theorem criticalMassJ_characterization {T ρ c d_sq : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq) (hρ : ρ < 1) :
    2 * criticalMassJ T ρ c d_sq * c ^ 2 * d_sq / (1 - ρ) = T := by
  simp only [criticalMassJ]
  have h1ρ : (0 : ℝ) ≠ 1 - ρ := by linarith
  have hcd : 0 < 2 * c ^ 2 * d_sq := by positivity
  field_simp

Dependency Graph

Location

thesis/CESProofs/EntryExit/Defs.lean:88

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file