IndisputableMonolith.NavierStokes.RM2U.ProjectedPDE

   1import IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity
   2
   3/-!
   4# RM2U.ProjectedPDE (hypothesis interface layer)
   5
   6This file does **not** formalize the 3D Navier–Stokes projection yet. Instead it introduces a
   7Lean-facing *hypothesis interface* that matches the TeX lemma `lem:Ab-evolution`:
   8
   9> `(∂_t - Δ_r + 6/r^2) A = F`
  10
  11rewritten in our time-slice operator language as
  12
  13> `rm2uOp(P) = F - A_t`
  14
  15The point of this layer is purely *plumbing*: it turns separate bounds on the forcing pairing
  16and on the time-derivative pairing into the single “pairing bound” field required by
  17`TailFluxVanishImpliesCoerciveHypothesisAt`, which then unlocks the already-proved theorem
  18`coerciveL2Bound_of_tailFluxVanish`.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace NavierStokes
  23namespace RM2U
  24
  25open Filter MeasureTheory Set
  26open scoped Topology Interval
  27
  28/-!
  29## Projected PDE hypothesis interface
  30
  31Important Lean detail: `Prop`-valued structures cannot store data fields like functions.
  32So we parameterize the time-derivative/forcing functions explicitly.
  33-/
  34
  35/-- Hypothesis: the RM2U operator pairing can be bounded by splitting `rm2uOp = F - A_t`.
  36
  37This is intentionally *time-slice* and abstract: it doesn't define what `A_t`/`F` are, only that
  38they exist and can be paired against `A r^2` on `[a,R]`.
  39-/
  40structure ProjectedPDEPairingHypothesisAt (P : RM2URadialProfile) (a : ℝ)
  41    (At F : ℝ → ℝ) : Prop where
  42  /-- Pointwise relation on `(1,∞)`: `rm2uOp = F - At`. -/
  43  hDecomp : ∀ r ∈ Set.Ioi (1 : ℝ), rm2uOp P r = F r - At r
  44  /-- Interval-integrability of the forcing pairing on `[a,R]` (needed for linearity). -/
  45  hForceInt :
  46    ∀ R : ℝ, a ≤ R → IntervalIntegrable (fun x : ℝ => (F x) * (P.A x) * (x ^ 2)) volume a R
  47  /-- Interval-integrability of the time-derivative pairing on `[a,R]` (needed for linearity). -/
  48  hTimeInt :
  49    ∀ R : ℝ, a ≤ R → IntervalIntegrable (fun x : ℝ => (At x) * (P.A x) * (x ^ 2)) volume a R
  50  /-- Uniform bound on the forcing pairing on `[a,R]`. -/
  51  hForcePair :
  52    ∃ CF : ℝ, ∀ R : ℝ, a ≤ R → |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)| ≤ CF
  53  /-- Uniform bound on the time-derivative pairing on `[a,R]`. -/
  54  hTimePair :
  55    ∃ CT : ℝ, ∀ R : ℝ, a ≤ R → |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| ≤ CT
  56
  57/-- Build the `TailFluxVanishImpliesCoerciveHypothesisAt` interface from a projected PDE pairing
  58decomposition plus the remaining local/interval hypotheses.
  59
  60This isolates the *single* extra analytic step that the TeX manuscript is implicitly using:
  61bounding `∫ (F - A_t) A r^2` by bounding the two pairings separately.
  62-/
  63theorem TailFluxVanishImpliesCoerciveHypothesisAt.of_projectedPDEPairing
  64    (P : RM2URadialProfile) (a : ℝ)
  65    (hbase : TailFluxVanishImpliesCoerciveHypothesisAt P a)
  66    {At F : ℝ → ℝ} (hpde : ProjectedPDEPairingHypothesisAt P a At F) :
  67    TailFluxVanishImpliesCoerciveHypothesisAt P a := by
  68  classical
  69  refine
  70    { ha1 := hbase.ha1
  71      hA2_local := hbase.hA2_local
  72      hA'2_local := hbase.hA'2_local
  73      hA'_int := hbase.hA'_int
  74      hV'_int := hbase.hV'_int
  75      hf := hbase.hf
  76      hg := hbase.hg
  77      hPairBound := ?_ }
  78
  79  rcases hpde.hForcePair with ⟨CF, hCF⟩
  80  rcases hpde.hTimePair with ⟨CT, hCT⟩
  81  refine ⟨CF + CT, ?_⟩
  82  intro R haR
  83
  84  -- Rewrite `rm2uOp` to `F - At` on `[a,R]` (note: `[a,R] ⊆ (1,∞)` because `1 < a`).
  85  have hcongr :
  86      (∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)) =
  87        ∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2) := by
  88    refine intervalIntegral.integral_congr ?_
  89    intro x hx
  90    have hx' : x ∈ Set.Icc a R := by
  91      simpa [Set.uIcc_of_le haR] using hx
  92    have hx1 : x ∈ Set.Ioi (1 : ℝ) := lt_of_lt_of_le hbase.ha1 hx'.1
  93    simp [hpde.hDecomp x hx1]
  94
  95  -- Triangle inequality: split the pairing into force and time-derivative parts.
  96  have hsplit :
  97      |∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2)|
  98        ≤ |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)|
  99          + |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| := by
 100    -- `∫ ((F-At)*A*r^2) = ∫ (F*A*r^2) - ∫ (At*A*r^2)`.
 101    have hsub :
 102        (∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2)) =
 103          (∫ x in a..R, (F x) * (P.A x) * (x ^ 2))
 104            - ∫ x in a..R, (At x) * (P.A x) * (x ^ 2) := by
 105      -- pointwise: `(F-At)*A*r^2 = (F*A*r^2) - (At*A*r^2)`
 106      have hpt :
 107          (fun x : ℝ => ((F x) - (At x)) * (P.A x) * (x ^ 2)) =
 108            fun x : ℝ => (F x) * (P.A x) * (x ^ 2) - (At x) * (P.A x) * (x ^ 2) := by
 109        funext x
 110        ring
 111      -- linearity requires interval integrability
 112      simpa [hpt] using
 113        (intervalIntegral.integral_sub (μ := volume) (a := a) (b := R)
 114          (hf := hpde.hForceInt R haR) (hg := hpde.hTimeInt R haR))
 115
 116    -- `|u - v| = |u + (-v)| ≤ |u| + |v|`
 117    set u : ℝ := ∫ x in a..R, (F x) * (P.A x) * (x ^ 2)
 118    set v : ℝ := ∫ x in a..R, (At x) * (P.A x) * (x ^ 2)
 119    have : |u - v| ≤ |u| + |v| := by
 120      -- triangle inequality in `ℝ` written via the norm
 121      simpa [Real.norm_eq_abs, sub_eq_add_neg, u, v] using (norm_add_le u (-v))
 122    simpa [hsub, u, v] using this
 123
 124  calc
 125    |∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)|
 126        = |∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2)| := by
 127            simp [hcongr]
 128    _ ≤ |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)|
 129          + |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| := hsplit
 130    _ ≤ CF + CT := by
 131          exact add_le_add (hCF R haR) (hCT R haR)
 132
 133end RM2U
 134end NavierStokes
 135end IndisputableMonolith
 136