lambda_0

formal source

  42  J_curv lambda - J_bit_normalized
  43
  44/-- The balance point in RS-native dimensionless units. -/
  45noncomputable def lambda_0 : ℝ := 1 / Real.sqrt 2
  46
  47lemma lambda_0_pos : 0 < lambda_0 := by
  48  unfold lambda_0
  49  apply div_pos one_pos
  50  exact Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  51
  52/-- lambda_0² = 1/2. -/
  53lemma lambda_0_sq : lambda_0 ^ 2 = 1 / 2 := by
  54  unfold lambda_0
  55  rw [div_pow]
  56  have h2 : (0 : ℝ) ≤ 2 := by norm_num
  57  rw [Real.sq_sqrt h2]
  58  norm_num
  59
  60/-- The balance residual vanishes at lambda_0. -/
  61theorem balance_at_lambda_0 : balanceResidual lambda_0 = 0 := by
  62  unfold balanceResidual J_curv J_bit_normalized
  63  rw [lambda_0_sq]
  64  ring
  65
  66/-- lambda_0 is the unique positive root of the balance residual. -/
  67theorem balance_unique_positive_root (lambda : ℝ) (hlambda : lambda > 0) :
  68    balanceResidual lambda = 0 ↔ lambda = lambda_0 := by
  69  unfold balanceResidual J_curv J_bit_normalized lambda_0
  70  constructor
  71  · intro h
  72    have hsq : lambda ^ 2 = 1 / 2 := by linarith
  73    have hlam_sqrt : lambda = Real.sqrt (1 / 2) := by
  74      rw [← Real.sqrt_sq (le_of_lt hlambda), hsq]
  75    rw [hlam_sqrt, Real.sqrt_div (by norm_num : (0:ℝ) ≤ 1), Real.sqrt_one]