IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D

   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# Galerkin2D (Milestone M1)
   9
  10This file introduces a **finite-dimensional** (Fourier-mode truncated) model for 2D incompressible
  11Navier–Stokes on the torus.  The goal of M1 is *not* the continuum limit yet — it is to get a
  12concrete discrete state space and the basic algebraic energy identity for the inviscid case.
  13
  14Design choices (Lean-friendly):
  15- We represent the truncated Fourier modes as a `Finset` and then use the coercion
  16  `((modes N : Finset Mode) : Type*)` as the finite index type of coefficients.
  17- The nonlinear term is modeled as an abstract bilinear operator `B` together with the single
  18  algebraic property needed for inviscid energy conservation: `⟪B u u, u⟫ = 0`.
  19
  20This keeps the file executable/compilable while making the analytic content explicit for later
  21work (Milestones M2+).
  22-/
  23
  24namespace IndisputableMonolith.ClassicalBridge.Fluids
  25
  26open Real
  27open scoped InnerProductSpace
  28
  29/-!
  30## Truncated Fourier modes on 𝕋²
  31-/
  32
  33/-- A 2D Fourier mode (k₁, k₂). -/
  34abbrev Mode2 : Type := ℤ × ℤ
  35
  36/-- Truncation predicate: max(|k₁|,|k₂|) ≤ N. -/
  37def modeTrunc (N : ℕ) (k : Mode2) : Prop :=
  38  max k.1.natAbs k.2.natAbs ≤ N
  39
  40/-- The finite set of truncated modes. -/
  41noncomputable def modes (N : ℕ) : Finset Mode2 :=
  42  ((Finset.Icc (-((N : ℤ))) (N : ℤ)).product (Finset.Icc (-((N : ℤ))) (N : ℤ)))
  43
  44lemma mem_modes_iff {N : ℕ} {k : Mode2} :
  45    k ∈ modes N ↔ k.1 ∈ Finset.Icc (-((N : ℤ))) (N : ℤ) ∧ k.2 ∈ Finset.Icc (-((N : ℤ))) (N : ℤ) := by
  46  simp [modes, and_left_comm, and_assoc, and_comm]
  47
  48/-!
  49## Galerkin state space
  50-/
  51
  52-- We use Euclidean (L²) norms/inner products for energy identities, so we model coefficients
  53-- in `EuclideanSpace`, not plain Pi types (which carry the sup norm).
  54
  55/-- Velocity Fourier coefficient at a mode: a Euclidean real 2-vector (û₁, û₂). -/
  56abbrev VelCoeff : Type := EuclideanSpace ℝ (Fin 2)
  57
  58/-- The Galerkin state: velocity coefficients for each truncated mode and each component. -/
  59abbrev GalerkinState (N : ℕ) : Type :=
  60  EuclideanSpace ℝ ((modes N) × Fin 2)
  61
  62/-!
  63## Discrete dynamics
  64-/
  65
  66/-- Squared wave number \( |k|^2 \) as a real number. -/
  67noncomputable def kSq (k : Mode2) : ℝ :=
  68  (k.1 : ℝ) ^ 2 + (k.2 : ℝ) ^ 2
  69
  70/-- Fourier Laplacian on coefficients: (Δ û)(k) = -|k|² û(k). -/
  71noncomputable def laplacianCoeff {N : ℕ} (u : GalerkinState N) : GalerkinState N :=
  72  WithLp.toLp 2 (fun kc => (-kSq ((kc.1 : Mode2))) * u kc)
  73
  74/-- Abstract Galerkin convection operator (projected nonlinearity).
  75
  76Later we will replace this with the explicit Fourier convolution + Leray projection. -/
  77def ConvectionOp (N : ℕ) : Type :=
  78  GalerkinState N → GalerkinState N → GalerkinState N
  79
  80/-- Discrete Navier–Stokes RHS: u' = νΔu - B(u,u). -/
  81noncomputable def galerkinNSRHS {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : GalerkinState N) :
  82    GalerkinState N :=
  83  (ν • laplacianCoeff u) - (B u u)
  84
  85/-!
  86## Energy functional and inviscid conservation
  87-/
  88
  89/-- Discrete kinetic energy: \(E(u)=\frac12 \|u\|^2\). -/
  90noncomputable def discreteEnergy {N : ℕ} (u : GalerkinState N) : ℝ :=
  91  (1 / 2 : ℝ) * ‖u‖ ^ 2
  92
  93/-- Algebraic hypothesis capturing the skew-symmetry of the Galerkin nonlinearity in L²:
  94\( \langle B(u,u), u \rangle = 0 \). -/
  95structure EnergySkewHypothesis {N : ℕ} (B : ConvectionOp N) : Prop where
  96  skew : ∀ u : GalerkinState N, ⟪B u u, u⟫_ℝ = 0
  97
  98/-- Energy conservation for the inviscid Galerkin system (ν = 0), stated at a point.
  99
 100If `u` solves `u' = -B(u,u)` and the nonlinearity is energy-skew, then the derivative of the
 101discrete energy is zero.
 102-/
 103theorem inviscid_energy_deriv_zero {N : ℕ} (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 104    (u : ℝ → GalerkinState N) {t : ℝ}
 105    (hu : HasDerivAt u (-(B (u t) (u t))) t) :
 106    HasDerivAt (fun s => discreteEnergy (u s)) 0 t := by
 107  -- Use the chain rule for `‖u‖^2` in an inner product space.
 108  -- d/dt (1/2 * ‖u‖^2) = ⟪u', u⟫.
 109  have h_normsq :
 110      HasDerivAt (fun s => ‖u s‖ ^ 2) (2 * ⟪u t, -(B (u t) (u t))⟫_ℝ) t := by
 111    -- `HasDerivAt.norm_sq` gives: derivative of `‖u‖^2` is `2 * ⟪u, u'⟫`.
 112    simpa using (HasDerivAt.norm_sq hu)
 113  have h_energy : HasDerivAt (fun s => discreteEnergy (u s))
 114      ((1 / 2 : ℝ) * (2 * ⟪u t, -(B (u t) (u t))⟫_ℝ)) t := by
 115    -- Multiply the norm-square derivative by 1/2
 116    simpa [discreteEnergy, mul_assoc] using h_normsq.const_mul (1 / 2 : ℝ)
 117  -- Now simplify using skew-symmetry: ⟪-B(u,u), u⟫ = -⟪B(u,u),u⟫ = 0
 118  have h_inner_zero : ⟪u t, -(B (u t) (u t))⟫_ℝ = 0 := by
 119    calc
 120      ⟪u t, -(B (u t) (u t))⟫_ℝ = -⟪u t, B (u t) (u t)⟫_ℝ := by simp
 121      _ = -⟪B (u t) (u t), u t⟫_ℝ := by simp [real_inner_comm]
 122      _ = 0 := by simp [HB.skew (u t)]
 123  -- Conclude derivative is zero.
 124  simpa [h_inner_zero] using h_energy
 125
 126/-!
 127## Viscous energy dissipation (discrete Laplacian)
 128
 129For the 2D Galerkin system, the (Fourier) Laplacian is diagonal and dissipative:
 130`⟪u, Δu⟫ ≤ 0`.  This is the algebraic input behind uniform energy bounds.
 131-/
 132
 133lemma laplacianCoeff_inner_self_nonpos {N : ℕ} (u : GalerkinState N) :
 134    ⟪u, laplacianCoeff u⟫_ℝ ≤ 0 := by
 135  classical
 136  -- Expand the inner product as a finite sum over coordinates.
 137  -- For each coordinate `kc`, the contribution is `u kc * ((-kSq kc.1) * u kc)`,
 138  -- which is nonpositive since `kSq ≥ 0` and `u kc * u kc ≥ 0`.
 139  have hsum :
 140      ⟪u, laplacianCoeff u⟫_ℝ =
 141        ∑ kc : (modes N) × Fin 2, u kc * ((-kSq (kc.1 : Mode2)) * u kc) := by
 142    -- `PiLp.inner_apply` expands the inner product; `laplacianCoeff` is defined via `WithLp.toLp`.
 143    -- The evaluation lemma `PiLp.toLp_apply` is `rfl`, so `simp` reduces the application.
 144    simp [laplacianCoeff, PiLp.inner_apply, kSq, mul_comm, mul_left_comm]
 145  -- Reduce to a sum of nonpositive terms.
 146  rw [hsum]
 147  refine Finset.sum_nonpos ?_
 148  intro kc _hkc
 149  have hkSq : 0 ≤ kSq (kc.1 : Mode2) := by
 150    -- kSq = k₁² + k₂²
 151    simp [kSq, add_nonneg, sq_nonneg]
 152  have hkneg : (-kSq (kc.1 : Mode2)) ≤ 0 := by linarith
 153  have hmul : 0 ≤ u kc * u kc := mul_self_nonneg (u kc)
 154  calc
 155    u kc * ((-kSq (kc.1 : Mode2)) * u kc)
 156        = (-kSq (kc.1 : Mode2)) * (u kc * u kc) := by ring
 157    _ ≤ 0 := mul_nonpos_of_nonpos_of_nonneg hkneg hmul
 158
 159theorem viscous_energy_deriv_le_zero {N : ℕ} (ν : ℝ) (_hν : 0 ≤ ν)
 160    (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 161    (u : ℝ → GalerkinState N) {t : ℝ}
 162    (hu : HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
 163    HasDerivAt (fun s => discreteEnergy (u s)) (ν * ⟪u t, laplacianCoeff (u t)⟫_ℝ) t := by
 164  -- Differentiate `E(u)=1/2‖u‖^2` using `HasDerivAt.norm_sq`, then expand the RHS.
 165  have h_normsq :
 166      HasDerivAt (fun s => ‖u s‖ ^ 2) (2 * ⟪u t, galerkinNSRHS ν B (u t)⟫_ℝ) t := by
 167    simpa using (HasDerivAt.norm_sq hu)
 168  have h_energy :
 169      HasDerivAt (fun s => discreteEnergy (u s)) ((1 / 2 : ℝ) * (2 * ⟪u t, galerkinNSRHS ν B (u t)⟫_ℝ)) t := by
 170    simpa [discreteEnergy, mul_assoc] using h_normsq.const_mul (1 / 2 : ℝ)
 171  -- Now simplify the inner product with `galerkinNSRHS`.
 172  -- `⟪u, νΔu - B(u,u)⟫ = ν⟪u,Δu⟫ - ⟪u,B(u,u)⟫` and skew gives the second term is 0.
 173  have h_skew' : ⟪u t, B (u t) (u t)⟫_ℝ = 0 := by
 174    -- Convert `⟪B u u, u⟫ = 0` to `⟪u, B u u⟫ = 0` using symmetry.
 175    have : ⟪B (u t) (u t), u t⟫_ℝ = 0 := HB.skew (u t)
 176    simpa [real_inner_comm] using this
 177  have h_inner :
 178      ⟪u t, galerkinNSRHS ν B (u t)⟫_ℝ = ν * ⟪u t, laplacianCoeff (u t)⟫_ℝ := by
 179    simp [galerkinNSRHS, inner_sub_right, inner_smul_right, h_skew']
 180  -- Finish by rewriting.
 181  simpa [h_inner, mul_assoc, mul_left_comm, mul_comm] using h_energy
 182
 183theorem viscous_energy_deriv_nonpos {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 184    (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 185    (u : ℝ → GalerkinState N) {t : ℝ}
 186    (hu : HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
 187    HasDerivAt (fun s => discreteEnergy (u s)) (ν * ⟪u t, laplacianCoeff (u t)⟫_ℝ) t ∧
 188      ν * ⟪u t, laplacianCoeff (u t)⟫_ℝ ≤ 0 := by
 189  refine ⟨viscous_energy_deriv_le_zero (N := N) ν hν B HB u hu, ?_⟩
 190  have hL : ⟪u t, laplacianCoeff (u t)⟫_ℝ ≤ 0 := laplacianCoeff_inner_self_nonpos (u := u t)
 191  exact mul_nonpos_of_nonneg_of_nonpos hν hL
 192
 193theorem viscous_energy_antitone {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 194    (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 195    (u : ℝ → GalerkinState N)
 196    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
 197    Antitone (fun t => discreteEnergy (u t)) := by
 198  -- Use the calculus lemma `antitone_of_hasDerivAt_nonpos`.
 199  refine antitone_of_hasDerivAt_nonpos (f := fun t => discreteEnergy (u t))
 200      (f' := fun t => ν * ⟪u t, laplacianCoeff (u t)⟫_ℝ) ?_ ?_
 201  · intro t
 202    exact viscous_energy_deriv_le_zero (N := N) ν hν B HB u (hu t)
 203  · intro t
 204    have hL : ⟪u t, laplacianCoeff (u t)⟫_ℝ ≤ 0 :=
 205      laplacianCoeff_inner_self_nonpos (u := u t)
 206    exact mul_nonpos_of_nonneg_of_nonpos hν hL
 207
 208theorem viscous_energy_bound_from_initial {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 209    (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 210    (u : ℝ → GalerkinState N)
 211    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
 212    ∀ t ≥ 0, discreteEnergy (u t) ≤ discreteEnergy (u 0) := by
 213  intro t ht
 214  have hAnti : Antitone (fun s => discreteEnergy (u s)) :=
 215    viscous_energy_antitone (N := N) ν hν B HB u hu
 216  -- Antitone: s₁ ≤ s₂ → f s₂ ≤ f s₁
 217  have : discreteEnergy (u t) ≤ discreteEnergy (u 0) := hAnti ht
 218  simpa using this
 219
 220theorem viscous_norm_bound_from_initial {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 221    (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 222    (u : ℝ → GalerkinState N)
 223    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
 224    ∀ t ≥ 0, ‖u t‖ ≤ ‖u 0‖ := by
 225  intro t ht
 226  have hE : discreteEnergy (u t) ≤ discreteEnergy (u 0) :=
 227    viscous_energy_bound_from_initial (N := N) ν hν B HB u hu t ht
 228  have hE' : (1 / 2 : ℝ) * ‖u t‖ ^ 2 ≤ (1 / 2 : ℝ) * ‖u 0‖ ^ 2 := by
 229    simpa [discreteEnergy] using hE
 230  -- Multiply both sides by `2` to cancel the `1/2`.
 231  have hsq : ‖u t‖ ^ 2 ≤ ‖u 0‖ ^ 2 := by
 232    have hmul := mul_le_mul_of_nonneg_left hE' (by norm_num : (0 : ℝ) ≤ 2)
 233    -- `2 * (1/2) = 1`
 234    simpa [mul_assoc] using hmul
 235  -- Convert the square inequality to a norm inequality (norms are nonnegative).
 236  exact le_of_sq_le_sq hsq (norm_nonneg (u 0))
 237
 238end IndisputableMonolith.ClassicalBridge.Fluids
 239