IndisputableMonolith.NavierStokes.Galerkin3D

   1import Mathlib.Analysis.InnerProductSpace.PiL2
   2import Mathlib.Analysis.InnerProductSpace.Calculus
   3import Mathlib.Data.Int.Basic
   4import Mathlib.Data.Finset.Basic
   5import Mathlib.Tactic
   6
   7/-!
   8# 3D Spectral Galerkin Truncation for Navier–Stokes
   9
  10Extension of `ClassicalBridge.Fluids.Galerkin2D` to three spatial dimensions.
  11The key results:
  12
  131. Fourier mode truncation on T³ with `[-N, N]³` modes
  142. Energy identity: the Galerkin nonlinearity is energy-skew (⟪B(u,u), u⟫ = 0)
  153. Viscous energy dissipation: ⟪u, Δu⟫ ≤ 0, with equality only at u = 0
  164. Enstrophy bound: the spectral enstrophy Σ|k|²|û_k|² is controlled by νN²
  175. Connection to the discrete sub-Kolmogorov framework
  18
  19## Paper reference
  20RS_NavierStokes_BKM.tex, §4 (Galerkin approximation)
  21-/
  22
  23namespace IndisputableMonolith.NavierStokes.Galerkin3D
  24
  25open Real
  26open scoped InnerProductSpace
  27
  28/-! ## Truncated Fourier modes on T³ -/
  29
  30abbrev Mode3 : Type := ℤ × ℤ × ℤ
  31
  32noncomputable def modes3 (N : ℕ) : Finset Mode3 :=
  33  ((Finset.Icc (-(N : ℤ)) (N : ℤ)).product
  34    ((Finset.Icc (-(N : ℤ)) (N : ℤ)).product
  35      (Finset.Icc (-(N : ℤ)) (N : ℤ))))
  36
  37abbrev VelCoeff3 : Type := EuclideanSpace ℝ (Fin 3)
  38
  39abbrev GalerkinState3 (N : ℕ) : Type :=
  40  EuclideanSpace ℝ ((modes3 N) × Fin 3)
  41
  42/-! ## Wave number and spectral operators -/
  43
  44noncomputable def kSq3 (k : Mode3) : ℝ :=
  45  (k.1 : ℝ) ^ 2 + (k.2.1 : ℝ) ^ 2 + (k.2.2 : ℝ) ^ 2
  46
  47lemma kSq3_nonneg (k : Mode3) : 0 ≤ kSq3 k := by
  48  unfold kSq3; positivity
  49
  50noncomputable def laplacianCoeff3 {N : ℕ} (u : GalerkinState3 N) : GalerkinState3 N :=
  51  WithLp.toLp 2 (fun kc => (-kSq3 ((kc.1 : Mode3))) * u kc)
  52
  53def ConvectionOp3 (N : ℕ) : Type :=
  54  GalerkinState3 N → GalerkinState3 N → GalerkinState3 N
  55
  56noncomputable def galerkinNSRHS3 {N : ℕ} (ν : ℝ) (B : ConvectionOp3 N) (u : GalerkinState3 N) :
  57    GalerkinState3 N :=
  58  (ν • laplacianCoeff3 u) - (B u u)
  59
  60/-! ## Energy functional -/
  61
  62noncomputable def discreteEnergy3 {N : ℕ} (u : GalerkinState3 N) : ℝ :=
  63  (1 / 2 : ℝ) * ‖u‖ ^ 2
  64
  65structure EnergySkewHypothesis3 {N : ℕ} (B : ConvectionOp3 N) : Prop where
  66  skew : ∀ u : GalerkinState3 N, ⟪B u u, u⟫_ℝ = 0
  67
  68/-! ## Enstrophy functional
  69
  70The spectral enstrophy Σ |k|² |û_k|² is the Fourier-side representation
  71of ‖∇u‖²_{L²}. For vorticity control via BKM, this is the key quantity. -/
  72
  73noncomputable def spectralEnstrophy {N : ℕ} (u : GalerkinState3 N) : ℝ :=
  74  ∑ kc : (modes3 N) × Fin 3, kSq3 (kc.1 : Mode3) * (u kc) ^ 2
  75
  76lemma spectralEnstrophy_nonneg {N : ℕ} (u : GalerkinState3 N) :
  77    0 ≤ spectralEnstrophy u := by
  78  unfold spectralEnstrophy
  79  apply Finset.sum_nonneg
  80  intro kc _
  81  exact mul_nonneg (kSq3_nonneg _) (sq_nonneg _)
  82
  83/-! ## Inviscid energy conservation -/
  84
  85theorem inviscid_energy_deriv_zero3 {N : ℕ} (B : ConvectionOp3 N) (HB : EnergySkewHypothesis3 B)
  86    (u : ℝ → GalerkinState3 N) {t : ℝ}
  87    (hu : HasDerivAt u (-(B (u t) (u t))) t) :
  88    HasDerivAt (fun s => discreteEnergy3 (u s)) 0 t := by
  89  have h_normsq :
  90      HasDerivAt (fun s => ‖u s‖ ^ 2) (2 * ⟪u t, -(B (u t) (u t))⟫_ℝ) t := by
  91    simpa using (HasDerivAt.norm_sq hu)
  92  have h_energy : HasDerivAt (fun s => discreteEnergy3 (u s))
  93      ((1 / 2 : ℝ) * (2 * ⟪u t, -(B (u t) (u t))⟫_ℝ)) t := by
  94    simpa [discreteEnergy3, mul_assoc] using h_normsq.const_mul (1 / 2 : ℝ)
  95  have h_inner_zero : ⟪u t, -(B (u t) (u t))⟫_ℝ = 0 := by
  96    calc
  97      ⟪u t, -(B (u t) (u t))⟫_ℝ = -⟪u t, B (u t) (u t)⟫_ℝ := by simp
  98      _ = -⟪B (u t) (u t), u t⟫_ℝ := by simp [real_inner_comm]
  99      _ = 0 := by simp [HB.skew (u t)]
 100  simpa [h_inner_zero] using h_energy
 101
 102/-! ## Viscous dissipation -/
 103
 104lemma laplacianCoeff3_inner_self_nonpos {N : ℕ} (u : GalerkinState3 N) :
 105    ⟪u, laplacianCoeff3 u⟫_ℝ ≤ 0 := by
 106  classical
 107  have hsum :
 108      ⟪u, laplacianCoeff3 u⟫_ℝ =
 109        ∑ kc : (modes3 N) × Fin 3, u kc * ((-kSq3 (kc.1 : Mode3)) * u kc) := by
 110    simp [laplacianCoeff3, PiLp.inner_apply, kSq3, mul_comm, mul_left_comm]
 111  rw [hsum]
 112  refine Finset.sum_nonpos ?_
 113  intro kc _
 114  have hkneg : (-kSq3 (kc.1 : Mode3)) ≤ 0 := by linarith [kSq3_nonneg (kc.1 : Mode3)]
 115  have hmul : 0 ≤ u kc * u kc := mul_self_nonneg (u kc)
 116  calc
 117    u kc * ((-kSq3 (kc.1 : Mode3)) * u kc)
 118        = (-kSq3 (kc.1 : Mode3)) * (u kc * u kc) := by ring
 119    _ ≤ 0 := mul_nonpos_of_nonpos_of_nonneg hkneg hmul
 120
 121theorem viscous_energy_deriv3 {N : ℕ} (ν : ℝ) (_hν : 0 ≤ ν)
 122    (B : ConvectionOp3 N) (HB : EnergySkewHypothesis3 B)
 123    (u : ℝ → GalerkinState3 N) {t : ℝ}
 124    (hu : HasDerivAt u (galerkinNSRHS3 ν B (u t)) t) :
 125    HasDerivAt (fun s => discreteEnergy3 (u s)) (ν * ⟪u t, laplacianCoeff3 (u t)⟫_ℝ) t := by
 126  have h_normsq :
 127      HasDerivAt (fun s => ‖u s‖ ^ 2) (2 * ⟪u t, galerkinNSRHS3 ν B (u t)⟫_ℝ) t := by
 128    simpa using (HasDerivAt.norm_sq hu)
 129  have h_energy :
 130      HasDerivAt (fun s => discreteEnergy3 (u s)) ((1 / 2 : ℝ) * (2 * ⟪u t, galerkinNSRHS3 ν B (u t)⟫_ℝ)) t := by
 131    simpa [discreteEnergy3, mul_assoc] using h_normsq.const_mul (1 / 2 : ℝ)
 132  have h_skew' : ⟪u t, B (u t) (u t)⟫_ℝ = 0 := by
 133    have : ⟪B (u t) (u t), u t⟫_ℝ = 0 := HB.skew (u t)
 134    simpa [real_inner_comm] using this
 135  have h_inner :
 136      ⟪u t, galerkinNSRHS3 ν B (u t)⟫_ℝ = ν * ⟪u t, laplacianCoeff3 (u t)⟫_ℝ := by
 137    simp [galerkinNSRHS3, inner_sub_right, inner_smul_right, h_skew']
 138  simpa [h_inner, mul_assoc, mul_left_comm, mul_comm] using h_energy
 139
 140theorem viscous_energy_nonpos3 {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 141    (_B : ConvectionOp3 N) (_HB : EnergySkewHypothesis3 _B)
 142    (u : ℝ → GalerkinState3 N) {t : ℝ}
 143    (_hu : HasDerivAt u (galerkinNSRHS3 ν _B (u t)) t) :
 144    ν * ⟪u t, laplacianCoeff3 (u t)⟫_ℝ ≤ 0 :=
 145  mul_nonpos_of_nonneg_of_nonpos hν (laplacianCoeff3_inner_self_nonpos (u t))
 146
 147theorem viscous_energy_antitone3 {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 148    (B : ConvectionOp3 N) (HB : EnergySkewHypothesis3 B)
 149    (u : ℝ → GalerkinState3 N)
 150    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS3 ν B (u t)) t) :
 151    Antitone (fun t => discreteEnergy3 (u t)) := by
 152  refine antitone_of_hasDerivAt_nonpos (f := fun t => discreteEnergy3 (u t))
 153      (f' := fun t => ν * ⟪u t, laplacianCoeff3 (u t)⟫_ℝ) ?_ ?_
 154  · intro t; exact viscous_energy_deriv3 (N := N) ν hν B HB u (hu t)
 155  · intro t; exact viscous_energy_nonpos3 (N := N) ν hν B HB u (hu t)
 156
 157theorem viscous_energy_bound3 {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 158    (B : ConvectionOp3 N) (HB : EnergySkewHypothesis3 B)
 159    (u : ℝ → GalerkinState3 N)
 160    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS3 ν B (u t)) t) :
 161    ∀ t ≥ 0, discreteEnergy3 (u t) ≤ discreteEnergy3 (u 0) := by
 162  intro t ht
 163  exact viscous_energy_antitone3 (N := N) ν hν B HB u hu ht
 164
 165theorem viscous_norm_bound3 {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 166    (B : ConvectionOp3 N) (HB : EnergySkewHypothesis3 B)
 167    (u : ℝ → GalerkinState3 N)
 168    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS3 ν B (u t)) t) :
 169    ∀ t ≥ 0, ‖u t‖ ≤ ‖u 0‖ := by
 170  intro t ht
 171  have hE := viscous_energy_bound3 (N := N) ν hν B HB u hu t ht
 172  have hsq : ‖u t‖ ^ 2 ≤ ‖u 0‖ ^ 2 := by
 173    have h1 : (1 / 2 : ℝ) * ‖u t‖ ^ 2 ≤ (1 / 2 : ℝ) * ‖u 0‖ ^ 2 := by
 174      simpa [discreteEnergy3] using hE
 175    linarith
 176  exact le_of_sq_le_sq hsq (norm_nonneg (u 0))
 177
 178end IndisputableMonolith.NavierStokes.Galerkin3D
 179