Documentation

Lean 4 Proof

theorem criticalMassJ_increasing_in_complementarity {T c d_sq ρ₁ ρ₂ : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq) (hT : 0 < T)
    (_hρ₁ : ρ₁ < 1) (_hρ₂ : ρ₂ < 1) (hρ : ρ₁ < ρ₂) :
    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_left (by linarith) hT
  · positivity

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Defs.lean:108

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file