IndisputableMonolith.NavierStokes.RM2U.RM2Closure

   1import IndisputableMonolith.NavierStokes.RM2U.Core
   2
   3/-!
   4# RM2U.RM2Closure (interface layer)
   5
   6This file is meant to host the fully classical “coercive \(\ell=2\) ⇒ RM2” closure steps
   7from `navier-dec-12-rewrite.tex`, namely:
   8
   9- coercive \(\ell=2\) control ⇒ finiteness of the log-critical shell moment `∫ |A|/r`,
  10- finiteness of that shell moment ⇒ boundedness of the affine/harmonic obstruction (RM2).
  11
  12For now, we keep the final “RM2 statement” abstract and provide a single *interface* hypothesis
  13to prevent scattering assumptions across the codebase. The plan is to later replace this
  14hypothesis with explicit proofs mirroring the TeX.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NavierStokes
  19namespace RM2U
  20
  21open MeasureTheory Set
  22
  23/-- Placeholder definition of “RM2 is closed” for a time-slice coefficient.
  24
  25In the manuscript, RM2 is equivalent to boundedness of the log-critical \(\ell=2\) tail moment.
  26We encode that equivalence in the simplest Lean-friendly way:
  27
  28`RM2Closed A := LogCriticalMomentFinite A`.
  29
  30Later we can refine this to match a more explicit fixed-frame compactness statement. -/
  31def RM2Closed (A : ℝ → ℝ) : Prop :=
  32  LogCriticalMomentFinite A
  33
  34/-- **Coercive \(\ell=2\) control ⇒ log-critical moment finiteness (RM2 in this simplified model).**
  35
  36This is the Lean translation of the manuscript’s one-line Cauchy–Schwarz argument:
  37
  38If `A ∈ L²((1,∞),dr)`, then `A/r ∈ L¹((1,∞),dr)` since `1/r ∈ L²((1,∞),dr)`.
  39
  40We package it in a way that is robust to later refactors of what “RM2 closed” means:
  41at minimum, coercive control implies the log-critical shell moment is absolutely convergent.
  42-/
  43theorem rm2Closed_of_coerciveL2Bound (P : RM2URadialProfile) :
  44    CoerciveL2Bound P → RM2Closed P.A := by
  45  intro hco
  46  -- Unpack the L² control of `A`.
  47  have hA2 : IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi (1 : ℝ)) volume :=
  48    hco.1
  49
  50  -- We will dominate `‖A(r)/r‖` by `A(r)^2 + r^(-2)` on `r > 1`.
  51  -- First, record integrability of `r ^ (-2)` (real power) on `(1,∞)`.
  52  have hRpow : IntegrableOn (fun r : ℝ => r ^ (-2 : ℝ)) (Set.Ioi (1 : ℝ)) volume := by
  53    -- `(-2) < -1`, so the real power is integrable at infinity.
  54    have hlt : (-2 : ℝ) < -1 := by linarith
  55    simpa using (integrableOn_Ioi_rpow_of_lt (a := (-2 : ℝ)) (c := (1 : ℝ)) hlt zero_lt_one)
  56
  57  have hdom : IntegrableOn (fun r : ℝ => (P.A r) ^ 2 + r ^ (-2 : ℝ)) (Set.Ioi (1 : ℝ)) volume :=
  58    hA2.add hRpow
  59
  60  -- `A/r` is continuous on `(1,∞)` (hence ae-strongly measurable on that set),
  61  -- because `HasDerivAt` implies continuity pointwise.
  62  have hcontA : ContinuousOn P.A (Set.Ioi (1 : ℝ)) := by
  63    intro x hx
  64    exact (P.hA x hx).continuousAt.continuousWithinAt
  65
  66  have hcontInv : ContinuousOn (fun r : ℝ => r⁻¹) (Set.Ioi (1 : ℝ)) := by
  67    -- `inv` is continuous away from `0`; `(1,∞) ⊆ {0}ᶜ`.
  68    refine (continuousOn_inv₀ : ContinuousOn (Inv.inv : ℝ → ℝ) ({0}ᶜ)).mono ?_
  69    intro r hr
  70    have : (r : ℝ) ≠ 0 := ne_of_gt (lt_trans (by norm_num : (0 : ℝ) < 1) (mem_Ioi.1 hr))
  71    simpa [Set.mem_compl_singleton_iff] using this
  72
  73  have hcontDiv : ContinuousOn (fun r : ℝ => P.A r / r) (Set.Ioi (1 : ℝ)) := by
  74    -- `A/r = A * r⁻¹`.
  75    simpa [div_eq_mul_inv] using hcontA.mul hcontInv
  76
  77  have hf_meas : AEStronglyMeasurable (fun r : ℝ => P.A r / r)
  78      (MeasureTheory.volume.restrict (Set.Ioi (1 : ℝ))) := by
  79    exact hcontDiv.aestronglyMeasurable measurableSet_Ioi
  80
  81  -- Pointwise domination on `(1,∞)`:
  82  -- `‖A/r‖ = |A| * r^(-1) ≤ |A|^2 + (r^(-1))^2 = A^2 + r^(-2)`.
  83  have h_le :
  84      ∀ᵐ r : ℝ ∂(MeasureTheory.volume.restrict (Set.Ioi (1 : ℝ))),
  85        ‖P.A r / r‖ ≤ (P.A r) ^ 2 + r ^ (-2 : ℝ) := by
  86    refine (ae_restrict_mem measurableSet_Ioi).mono ?_
  87    intro r hr
  88    have hr0 : 0 ≤ r := le_trans (by norm_num : (0 : ℝ) ≤ 1) (mem_Ioi.1 hr).le
  89    have hrpos : 0 < r := lt_trans (by norm_num : (0 : ℝ) < 1) (mem_Ioi.1 hr)
  90    -- Rewrite norms as abs; keep `|A| / r` form for easier final `simp`.
  91    simp only [Real.norm_eq_abs, abs_div, abs_of_pos hrpos]
  92    -- Reduce to an AM-GM style inequality.
  93    -- Let a = |A r|, b = r^(-1).
  94    have ha : 0 ≤ |P.A r| := abs_nonneg (P.A r)
  95    have hb : 0 ≤ r ^ (-1 : ℝ) := by
  96      -- real power of a nonnegative base is nonnegative
  97      exact Real.rpow_nonneg hr0 (-1 : ℝ)
  98    -- `|A| * r^(-1) ≤ |A|^2 + (r^(-1))^2` using `two_mul_le_add_sq` and `ab ≤ 2ab`.
  99    have hab0 : 0 ≤ |P.A r| * (r ^ (-1 : ℝ)) := mul_nonneg ha hb
 100    have h2 : 2 * |P.A r| * (r ^ (-1 : ℝ)) ≤ |P.A r| ^ 2 + (r ^ (-1 : ℝ)) ^ 2 :=
 101      two_mul_le_add_sq (|P.A r|) (r ^ (-1 : ℝ))
 102    have h1 : |P.A r| * (r ^ (-1 : ℝ)) ≤ 2 * |P.A r| * (r ^ (-1 : ℝ)) := by
 103      -- since `0 ≤ ab`, we have `ab ≤ 2ab`
 104      nlinarith
 105    have hmain : |P.A r| * (r ^ (-1 : ℝ)) ≤ |P.A r| ^ 2 + (r ^ (-1 : ℝ)) ^ 2 :=
 106      le_trans h1 h2
 107    -- Rewrite `(r^(-1))^2` as `r^(-2)` and `|A|^2` as `A^2`.
 108    have hrpow2 : (r ^ (-1 : ℝ)) ^ 2 = r ^ (-2 : ℝ) := by
 109      -- `r^(-2) = (r^(-1))^2` for `r ≥ 0`
 110      have : r ^ ((-1 : ℝ) * (2 : ℝ)) = (r ^ (-1 : ℝ)) ^ (2 : ℝ) :=
 111        (Real.rpow_mul (x := r) hr0 (-1 : ℝ) (2 : ℝ))
 112      -- convert real exponent `2` to nat power `2`
 113      simpa [show (-1 : ℝ) * (2 : ℝ) = (-2 : ℝ) by ring, Real.rpow_two] using this.symm
 114    -- Convert `|A| / r` to `|A| * r⁻¹` and compare `r⁻¹` with `r ^ (-1)`.
 115    have hdiv : |P.A r| / r = |P.A r| * r⁻¹ := by
 116      simp [div_eq_mul_inv]
 117
 118    -- On `r > 0`, `r ^ (-1 : ℝ) = r⁻¹`.
 119    have hrpow1 : r ^ (-1 : ℝ) = r⁻¹ := by
 120      simpa using (Real.rpow_neg_one r)
 121
 122    -- Finish: rewrite everything into the target shape.
 123    -- `|A|^2 = A^2` in ℝ, and `(r⁻¹)^2 = (r^2)⁻¹`.
 124    -- Also use `hrpow2` to replace `(r^(-1))^2` by `r^(-2)`.
 125    -- We keep the RHS as `A^2 + r^(-2)` to match the outer goal.
 126    have : |P.A r| / r ≤ (P.A r) ^ 2 + r ^ (-2 : ℝ) := by
 127      -- start from the inequality on `|A| * r^(-1)`
 128      have hmain' :
 129          |P.A r| * r⁻¹ ≤ |P.A r| ^ 2 + (r⁻¹) ^ 2 := by
 130        -- replace `r^(-1)` with `r⁻¹` in `hmain`
 131        simpa [hrpow1] using hmain
 132      -- rewrite the RHS and LHS into the requested form
 133      -- `(r⁻¹)^2 = (r^2)⁻¹`, and `(P.A r)^2 = |P.A r|^2`.
 134      -- Then replace `(r⁻¹)^2` by `r^(-2)` via `hrpow2`.
 135      -- Finally convert `|A|*r⁻¹` to `|A|/r`.
 136      -- Note: `hrpow2` is about `r^(-1)` not `r⁻¹`; use `hrpow1` to bridge.
 137      have hrpow2' : (r⁻¹) ^ 2 = r ^ (-2 : ℝ) := by
 138        -- `(r⁻¹)^2 = (r^(-1))^2 = r^(-2)`
 139        simpa [hrpow1] using hrpow2
 140      -- and `|A|^2 = A^2`
 141      have habs2 : |P.A r| ^ 2 = (P.A r) ^ 2 := by
 142        simp [pow_two]
 143      -- assemble
 144      calc
 145        |P.A r| / r = |P.A r| * r⁻¹ := hdiv
 146        _ ≤ |P.A r| ^ 2 + (r⁻¹) ^ 2 := hmain'
 147        _ = (P.A r) ^ 2 + r ^ (-2 : ℝ) := by
 148              simp [habs2, hrpow2']
 149    exact this
 150
 151  -- Conclude integrability by domination.
 152  -- We use the `Integrable.mono'` lemma on the restricted measure.
 153  have : Integrable (fun r : ℝ => P.A r / r) (MeasureTheory.volume.restrict (Set.Ioi (1 : ℝ))) :=
 154    (hdom.integrable).mono' hf_meas h_le
 155
 156  -- Repackage as `IntegrableOn` and match `RM2Closed`.
 157  simpa [RM2Closed, LogCriticalMomentFinite, IntegrableOn] using this
 158
 159/-- Interface hypothesis: coercive \(\ell=2\) control implies RM2 closure for this profile.
 160
 161This is *not* intended to remain an assumption long-term; it is a single placeholder
 162so that downstream developments can depend on one named lemma instead of ad hoc assumptions. -/
 163structure CoerciveImpliesRM2Hypothesis (P : RM2URadialProfile) : Prop where
 164  implies : CoerciveL2Bound P → RM2Closed P.A
 165
 166namespace CoerciveImpliesRM2Hypothesis
 167
 168/-- Construct the (now purely formal) interface hypothesis from the proved lemma
 169`rm2Closed_of_coerciveL2Bound`. This is here for backwards compatibility: downstream code can
 170depend on a named hypothesis while the file still remains `sorry`/`axiom` free. -/
 171theorem of_proved (P : RM2URadialProfile) : CoerciveImpliesRM2Hypothesis P :=
 172  ⟨rm2Closed_of_coerciveL2Bound (P := P)⟩
 173
 174end CoerciveImpliesRM2Hypothesis
 175
 176end RM2U
 177end NavierStokes
 178end IndisputableMonolith
 179