alpha_inv_phys_continuous

proof body

Tactic-mode proof.

  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)
  80        (Real.continuousAt_log hdiv_ne) hdiv_cont)
  81    have hscaled : ContinuousAt
  82        (fun q : ℝ => (1 / (3 * Real.pi)) * Real.log (q / Q_lock)) x := by
  83      exact hlog_cont.const_mul (1 / (3 * Real.pi))
  84    have hmain : ContinuousAt
  85        (fun q : ℝ => alpha_inv_running q Q_lock (1 / alpha_locked)) x := by
  86      simpa [alpha_inv_running] using continuousAt_const.sub hscaled
  87    exact hmain.continuousWithinAt
  88  have hg :
  89      ContinuousOn (fun _ : ℝ => (1 / alpha_locked : ℝ))
  90        (closure {x : ℝ | ¬x ≥ Q_lock}) := by
  91    simpa using (continuous_const.continuousOn :
  92      ContinuousOn (fun _ : ℝ => (1 / alpha_locked : ℝ))
  93        (closure {x : ℝ | ¬x ≥ Q_lock}))
  94  have hcont :
  95      Continuous (fun q : ℝ =>
  96        if Q_lock ≤ q then alpha_inv_running q Q_lock (1 / alpha_locked) else (1 / alpha_locked)) := by
  97    exact continuous_if hp hf hg
  98  have hEqFun :
  99      (fun q : ℝ =>
 100        if Q_lock ≤ q then alpha_inv_running q Q_lock (1 / alpha_locked) else (1 / alpha_locked))
 101        = alpha_inv_phys := by
 102    funext q
 103    simp [alpha_inv_phys, ge_iff_le]
 104  have hcontAt :
 105      ContinuousAt
 106        (fun q : ℝ =>
 107          if Q_lock ≤ q then alpha_inv_running q Q_lock (1 / alpha_locked) else (1 / alpha_locked))
 108        Q_lock := hcont.continuousAt
 109  rw [← hEqFun]
 110  exact hcontAt
 111
 112end CouplingLockIn
 113end Physics
 114end IndisputableMonolith