norm_extendByZero_le

formal source

 860global Euclidean norm of the truncated Galerkin state.
 861-/
 862
 863lemma norm_extendByZero_le {N : ℕ} (u : GalerkinState N) (k : Mode2) :
 864    ‖(extendByZero u) k‖ ≤ ‖u‖ := by
 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