solution_exists

proof body

Tactic-mode proof.

  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
  67        -- w_t is continuous everywhere
  68        apply Continuous.continuousOn
  69        unfold ILG.w_t ILG.w_t_with
  70        refine continuous_const.add ?_
  71        apply Continuous.mul continuous_const
  72        refine Continuous.sub ?_ continuous_const
  73
  74        -- rpow is continuous for positive base
  75        -- base is max eps_t (T/tau0) >= eps_t = 0.01 > 0
  76        apply Continuous.rpow
  77        · refine continuous_max continuous_const ?_
  78          exact continuous_id.div_const _
  79        · exact continuous_const
  80        · intro T; apply lt_max_of_lt_left; norm_num
  81      · exact continuousOn_const
  82
  83  -- 2. Existence of v_small such that f(v_small) < 0
  84  have hf_small_exists : ∃ v_small, 0 < v_small ∧ f v_small < 0 := by
  85    let v_bound := 2 * Real.pi * r / tau0
  86    let v_try := min (Real.sqrt (K / 2)) v_bound
  87    have hv_pos : 0 < v_try := by
  88      apply lt_min
  89      · exact Real.sqrt_pos.mpr (half_pos hK)
  90      · apply div_pos
  91        · exact mul_pos (mul_pos (by norm_num) Real.pi_pos) hr
  92        · exact htau
  93    use v_try
  94    constructor
  95    · exact hv_pos
  96    · have h_wt_ge_one : 1 ≤ ILG.w_t P (2 * Real.pi * r / v_try) tau0 := by
  97        apply ILG.w_t_ge_one P HP (2 * Real.pi * r / v_try) tau0 htau
  98        -- T >= tau0 <=> 2pi*r/v >= tau0 <=> 2pi*r/tau0 >= v
  99        rw [ge_iff_le]
 100        exact min_le_right _ _
 101
 102      unfold f
 103      -- f(v) = v^2 - w_t * K
 104      -- Since w_t >= 1, f(v) <= v^2 - K
 105      -- v^2 <= (sqrt(K/2))^2 = K/2
 106      have hv_sq : v_try^2 ≤ K / 2 := by
 107        have : v_try ≤ Real.sqrt (K / 2) := min_le_left _ _
 108        exact sq_le_sq_of_nonneg (le_of_lt (Real.sqrt_pos.mpr (half_pos hK))) this
 109
 110      have hfk : f v_try ≤ v_try^2 - K := by
 111        simp only [f, sub_le_sub_iff_left]
 112        exact (le_mul_iff_one_le_left hK).mpr h_wt_ge_one
 113
 114      calc f v_try ≤ v_try^2 - K := hfk
 115        _ ≤ K / 2 - K := sub_le_sub_right hv_sq K
 116        _ = -K / 2 := by ring
 117        _ < 0 := by linarith
 118
 119-- ... 75 more lines elided ...