norm_extendByZero_le

proof body

Tactic-mode proof.

 865  classical
 866  by_cases hk : k ∈ modes N
 867  ·
 868    have hext :
 869        (extendByZero u) k =
 870          !₂[u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2)),
 871             u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))] := by
 872      simp [extendByZero, coeffAt, hk]
 873
 874    have hsq_ext :
 875        ‖(extendByZero u) k‖ ^ 2 =
 876          ‖u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2))‖ ^ 2
 877            + ‖u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))‖ ^ 2 := by
 878      -- For `Fin 2`, `EuclideanSpace.norm_sq_eq` expands to the sum of the two coordinate squares.
 879      simp [hext, EuclideanSpace.norm_sq_eq, Fin.sum_univ_two]
 880
 881    have hnorm_u : ‖u‖ ^ 2 = ∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2 := by
 882      simp [EuclideanSpace.norm_sq_eq]
 883
 884    -- The 2-coordinate sum is bounded by the full coordinate sum.
 885    have hcoord_le :
 886        (‖u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2))‖ ^ 2
 887            + ‖u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))‖ ^ 2)
 888          ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := by
 889      let k' : (modes N) := ⟨k, hk⟩
 890      let s : Finset ((modes N) × Fin 2) :=
 891        insert (k', (⟨0, by decide⟩ : Fin 2)) ({(k', (⟨1, by decide⟩ : Fin 2))} : Finset ((modes N) × Fin 2))
 892      have hs : s ⊆ (Finset.univ : Finset ((modes N) × Fin 2)) := by
 893        intro x hx
 894        simp
 895      have hsum :
 896          (‖u (k', (⟨0, by decide⟩ : Fin 2))‖ ^ 2 + ‖u (k', (⟨1, by decide⟩ : Fin 2))‖ ^ 2)
 897            = (∑ kc ∈ s, ‖u kc‖ ^ 2) := by
 898        simp [s]
 899      have hle : (∑ kc ∈ s, ‖u kc‖ ^ 2) ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := by
 900        have hle' :
 901            (∑ kc ∈ s, ‖u kc‖ ^ 2)
 902              ≤ (∑ kc ∈ (Finset.univ : Finset ((modes N) × Fin 2)), ‖u kc‖ ^ 2) := by
 903          refine Finset.sum_le_sum_of_subset_of_nonneg hs ?_
 904          intro kc _hkc _hknot
 905          exact sq_nonneg ‖u kc‖
 906        simpa using hle'
 907      calc
 908        (‖u (k', (⟨0, by decide⟩ : Fin 2))‖ ^ 2 + ‖u (k', (⟨1, by decide⟩ : Fin 2))‖ ^ 2)
 909            = (∑ kc ∈ s, ‖u kc‖ ^ 2) := hsum
 910        _ ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := hle
 911
 912    have hsq_le : ‖(extendByZero u) k‖ ^ 2 ≤ ‖u‖ ^ 2 := by
 913      calc
 914        ‖(extendByZero u) k‖ ^ 2
 915            = (‖u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2))‖ ^ 2
 916                + ‖u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))‖ ^ 2) := hsq_ext
 917        _ ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := hcoord_le
 918        _ = ‖u‖ ^ 2 := by simp [hnorm_u]
 919
 920    exact le_of_sq_le_sq hsq_le (norm_nonneg u)
 921  ·
 922    -- Outside the truncation window the coefficient is zero, so the bound is trivial.
 923    have hnorm : ‖(extendByZero u) k‖ = 0 := by
 924      simp [extendByZero, coeffAt, hk]
 925    simp [hnorm, norm_nonneg u]
 926
 927/-!
 928## Compactness + identification as explicit hypotheses
 929-/
 930
 931/-- Hypothesis: uniform-in-`N` bounds for a *family* of Galerkin trajectories `uN`.
 932
 933In a real proof this would come from:
 934- discrete energy/enstrophy inequalities,
 935- CPM coercivity/dispersion bounds, and
 936- compactness tools (Aubin–Lions / Banach–Alaoglu / etc.).
 937-/