`extendByZero`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
domain: ClassicalBridge
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  52    0
  53
  54/-- Extend a truncated Galerkin state by zero to a full Fourier coefficient state. -/
  55noncomputable def extendByZero {N : ℕ} (u : GalerkinState N) : FourierState2D :=
  56  fun k =>
  57    -- Build a 2-vector coefficient from its two components.
  58    !₂[coeffAt u k ⟨0, by decide⟩, coeffAt u k ⟨1, by decide⟩]
  59
  60/-!
  61## Linearity of the zero-extension embedding
  62
  63We will eventually want to pass (linear) identities from Galerkin trajectories to limits.
  64For that, it is useful to record that `extendByZero` is a linear map.
  65-/
  66
  67lemma coeffAt_add {N : ℕ} (u v : GalerkinState N) (k : Mode2) (j : Fin 2) :
  68    coeffAt (u + v) k j = coeffAt u k j + coeffAt v k j := by
  69  classical
  70  by_cases hk : k ∈ modes N
  71  · simp [coeffAt, hk]
  72  · simp [coeffAt, hk]
  73
  74lemma coeffAt_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) (k : Mode2) (j : Fin 2) :
  75    coeffAt (c • u) k j = c * coeffAt u k j := by
  76  classical
  77  by_cases hk : k ∈ modes N
  78  · simp [coeffAt, hk]
  79  · simp [coeffAt, hk]
  80
  81lemma extendByZero_add {N : ℕ} (u v : GalerkinState N) :
  82    extendByZero (u + v) = extendByZero u + extendByZero v := by
  83  classical
  84  funext k
  85  ext j

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.