solution_exists

formal source

  33/-- **THEOREM: Existence of rotation velocity solution**
  34    For any radius r > 0 and enclosed mass M, there exists a velocity v
  35    that satisfies the ILG fixed-point equation. -/
  36theorem solution_exists (S : RotSys) (P : ILG.Params) (HP : ParamProps P) (tau0 : ℝ) (htau : 0 < tau0)
  37    (r : ℝ) (hr : 0 < r) (hM : 0 < S.Menc r) :
  38    ∃ v : ℝ, v > 0 ∧ is_ilg_vrot S P tau0 r v := by
  39  -- We use the Intermediate Value Theorem on the function f(v) = v^2 - w_t(r,v) * K
  40  -- where K = G * Menc / r > 0.
  41  let K := S.G * S.Menc r / r
  42  have hK : 0 < K := by
  43    apply div_pos
  44    · exact mul_pos S.posG hM
  45    · exact hr
  46
  47  let f : ℝ → ℝ := fun v => v^2 - ILG.w_t P (2 * Real.pi * r / v) tau0 * K
  48
  49  -- 1. Continuity of f on (0, inf)
  50  have h_cont : ContinuousOn f (Set.Ioi 0) := by
  51    apply ContinuousOn.sub
  52    · exact continuousOn_pow 2
  53    · apply ContinuousOn.mul
  54      · -- w_t is continuous. w_t(T, tau0) = 1 + Clag * ((max eps_t (T/tau0))^alpha - 1)
  55        -- T(v) = 2*pi*r / v is continuous on (0, inf)
  56        have hT : ContinuousOn (fun v => 2 * Real.pi * r / v) (Set.Ioi 0) := by
  57          apply ContinuousOn.div
  58          · exact continuousOn_const
  59          · exact continuousOn_id
  60          · intro v hv; exact ne_of_gt hv
  61
  62        -- Now compose with w_t
  63        -- w_t_with defaultConfig P T tau0
  64        -- = 1 + P.Clag * (Real.rpow (max defaultConfig.eps_t (T / tau0)) P.alpha - 1)
  65        refine ContinuousOn.comp (f := fun T => ILG.w_t P T tau0) (g := fun v => 2 * Real.pi * r / v) ?_ hT (Set.mapsTo_image _ _)
  66