alpha_inv_phys_continuous

formal source

  46/-- **THEOREM: Physical Coupling Continuity**
  47    The physical coupling is continuous at the lock-in boundary.
  48    Both branches agree at Q = Q_lock (proved in `alpha_lock_at_scale`). -/
  49theorem alpha_inv_phys_continuous :
  50    ContinuousAt alpha_inv_phys Q_lock := by
  51  have hQlock_pos : 0 < Q_lock := by
  52    simpa [Q_lock] using (effective_scale_pos ell0_pos)
  53  have hp :
  54      ∀ a ∈ frontier {x : ℝ | Q_lock ≤ x},
  55        alpha_inv_running a Q_lock (1 / alpha_locked) = (1 / alpha_locked) := by
  56    intro a ha
  57    have haIci : a ∈ frontier (Set.Ici Q_lock) := by
  58      simpa [Set.Ici] using ha
  59    have ha' : a ∈ ({Q_lock} : Set ℝ) := (frontier_Ici_subset (a := Q_lock)) haIci
  60    have hEq : a = Q_lock := by simpa using ha'
  61    subst hEq
  62    simpa [Q_lock] using alpha_lock_at_scale
  63  have hf :
  64      ContinuousOn
  65        (fun q : ℝ => alpha_inv_running q Q_lock (1 / alpha_locked))
  66        (closure {x : ℝ | Q_lock ≤ x}) := by
  67    intro x hx
  68    have hxClosure : x ∈ closure (Set.Ici Q_lock) := by
  69      simpa [Set.Ici] using hx
  70    have hxIci : x ∈ Set.Ici Q_lock := by
  71      simpa [closure_Ici] using hxClosure
  72    have hxge : Q_lock ≤ x := hxIci
  73    have hxpos : 0 < x := lt_of_lt_of_le hQlock_pos hxge
  74    have hdiv_ne : x / Q_lock ≠ 0 := by
  75      exact div_ne_zero (ne_of_gt hxpos) (ne_of_gt hQlock_pos)
  76    have hdiv_cont : ContinuousAt (fun q : ℝ => q / Q_lock) x := by
  77      exact continuousAt_id.div_const Q_lock
  78    have hlog_cont : ContinuousAt (fun q : ℝ => Real.log (q / Q_lock)) x := by
  79      exact (ContinuousAt.comp (f := fun q : ℝ => q / Q_lock) (g := Real.log) (x := x)