Uniform Sobolev energy bounds for all spatial derivatives of the Galerkin paths.

@[instance_reducible]

noncomputable def classicalSmoothLimitMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• classicalSmoothLimitMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem classicalSmoothLimitMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalSmoothLimitProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalSmoothLimitOneLeTwoFact : Fact (1 ≤ 2)

theorem AVenhance.Infra.Classical.GalerkinSmoothLimit.classicalSmoothLimitWord_periodic (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.GalerkinSmoothLimit.classicalSmoothLimitWord_contDiff (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ ⊤ f) : ContDiff ℝ (↑⊤) (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.GalerkinSmoothLimit.classicalSmoothLimitWord_memLp_eq_synthesis (N : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : let f := classicalWordDerivative w (realFourierModeAmbientExpansion N c); have hmem := ⋯; MeasureTheory.MemLp.toLp (Torus.periodicToTorus f) hmem = (Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N w) c)

theorem AVenhance.Infra.Classical.classicalGalerkinWordDerivative_gradient_energy_uniform_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (s : ℕ) : ∃ (E : ℝ), 0 ≤ E ∧ ∀ (N : ℕ), ∀ t ∈ Set.Icc 0 1, ∀ (w : List (Fin 2)), w.length ≤ s → gradNormSq (spaceGrad (classicalWordDerivative w (realFourierModeAmbientExpansion N (ODE.extendCurve classicalGalerkinWordDerivative_gradient_energy_uniform_bound._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)))) ≤ E

theorem AVenhance.Infra.Classical.classicalGalerkinWordDerivativeMap_norm_le (N : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : ‖(realFourierWordDerivativeMap N w) c‖ ≤ (2 * Real.pi * ↑N) ^ w.length * ‖c‖

Applying an ordered derivative word costs at most the corresponding cutoff frequency to that word's length in coefficient L².

theorem AVenhance.Infra.Classical.classicalGalerkinProjectionCLM_norm_le (N : ℕ) (v : ↥Parabolic.FourierGalerkin.ScalarTorusL2) : ‖(realFourierProjectionCLM N) v‖ ≤ ‖v‖

The finite Fourier coefficient projection is contractive on torus L².

theorem AVenhance.Infra.Classical.classicalGalerkinProjectionCLM_expansion (N K : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension K) (Parabolic.FourierGalerkin.realFourierModeFin K) (Torus.periodicToTorus (realFourierModeAmbientExpansion N c)) = (realFourierProjectionCLM K) ((Parabolic.FourierGalerkin.realFourierScalarMap N) c)

The L² coefficient projection of a finite ambient expansion is its continuous Fourier projection.

theorem AVenhance.Infra.Classical.classicalGalerkinWordDerivative_projectionCLM (N K : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : (Parabolic.FourierGalerkin.realFourierScalarMap K) ((realFourierWordDerivativeMap K w) ((realFourierProjectionCLM K) ((Parabolic.FourierGalerkin.realFourierScalarMap N) c))) = (Parabolic.FourierGalerkin.realFourierScalarMap K) (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension K) (Parabolic.FourierGalerkin.realFourierModeFin K) (Torus.periodicToTorus (classicalWordDerivative w (realFourierModeAmbientExpansion N c))))

Differentiating a finite Galerkin path and then projecting to cutoff K agrees with differentiating its cutoff-K projection.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinWordScalarPath (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (w : List (Fin 2)) (N : ℕ) : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)

The scalar L² path of one ordered spatial derivative of the finite Galerkin solutions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPath_apply (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (w : List (Fin 2)) (N : ℕ) (t : ↑(Set.Icc 0 1)) : (classicalGalerkinWordScalarPath φ hφ κ hκ F hF θ₀ hθ₀ w N) t = (Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N w) ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t))

noncomputable def AVenhance.Infra.Classical.classicalGalerkinLowDerivativeCLM (K : ℕ) (w : List (Fin 2)) : ↥Parabolic.FourierGalerkin.ScalarTorusL2 →L[ℝ] ↥Parabolic.FourierGalerkin.ScalarTorusL2

Project the base Galerkin path to a fixed cutoff, then apply one derivative word.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinLowDerivativeCLM_norm_apply_le (K : ℕ) (w : List (Fin 2)) (v : ↥Parabolic.FourierGalerkin.ScalarTorusL2) : ‖(classicalGalerkinLowDerivativeCLM K w) v‖ ≤ (2 * Real.pi * ↑K) ^ w.length * ‖v‖

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPath_tail_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (w : List (Fin 2)) (E : ℝ) (henergy : ∀ (N : ℕ), ∀ t ∈ Set.Icc 0 1, gradNormSq (spaceGrad (classicalWordDerivative w (realFourierModeAmbientExpansion N (ODE.extendCurve classicalGalerkinWordDerivative_gradient_energy_uniform_bound._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)))) ≤ E) (K N : ℕ) (hKN : K ≤ N) (t : ↑(Set.Icc 0 1)) : ‖(classicalGalerkinWordScalarPath φ hφ κ hκ F hF θ₀ hθ₀ w N) t - (classicalGalerkinLowDerivativeCLM K w) ((classicalGalerkinScalarPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)‖ ≤ √((4 * Real.pi ^ 2 * ↑(K + 1) ^ 2)⁻¹ * E)

Above a fixed cutoff, the derivative path differs from its low-mode projection by a tail controlled by the uniform energy of one more derivative.

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPathTailError_tendsto_zero (E : ℝ) : Filter.Tendsto (fun (K : ℕ) => √((4 * Real.pi ^ 2 * ↑(K + 1) ^ 2)⁻¹ * E)) Filter.atTop (nhds 0)

The derivative Fourier tail tends to zero as its lower cutoff increases.

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPath_cauchy (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) : CauchySeq fun (N : ℕ) => classicalGalerkinWordScalarPath φ hφ κ hκ F hF θ₀ hθ₀ w N

Every fixed ordered spatial derivative of the Galerkin paths is Cauchy in C([0,1];L²(T²)).

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPath_tendsto (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) : ∃ (u : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)), Filter.Tendsto (fun (N : ℕ) => classicalGalerkinWordScalarPath φ hφ κ hκ F hF θ₀ hθ₀ w N) Filter.atTop (nhds u)

noncomputable def AVenhance.Infra.Classical.classicalGalerkinWordScalarPathLimit (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)

Limit path for a spatial derivative word of the Galerkin solution.

Equations

• AVenhance.Infra.Classical.classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w = Classical.choose ⋯

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPathLimit_tendsto (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) : Filter.Tendsto (fun (N : ℕ) => classicalGalerkinWordScalarPath φ hφ κ hκ F hF θ₀ hθ₀ w N) Filter.atTop (nhds (classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w))

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPathLimit_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ↑(Set.Icc 0 1)), ‖(classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) t‖ ≤ C

theorem AVenhance.Infra.Classical.classicalComplexFourierCoeff_norm_le (f : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2) (k : Fin 2 → ℤ) : ‖UnitAddTorus.mFourierCoeff (↑↑f) k‖ ≤ ‖f‖

noncomputable def AVenhance.Infra.Classical.classicalRealToComplexTorusCLM : ↥Parabolic.FourierGalerkin.ScalarTorusL2 →L[ℝ] ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2

Embed real torus square-integrable functions into the complex space.

Equations

• AVenhance.Infra.Classical.classicalRealToComplexTorusCLM = ContinuousLinearMap.compLpL 2 MeasureTheory.volume Complex.ofRealCLM

noncomputable def AVenhance.Infra.Classical.classicalComplexFourierCoeffCLM (k : Fin 2 → ℤ) : ↥Parabolic.FourierGalerkin.ScalarTorusL2 →L[ℝ] ℂ

Extract a complex Fourier coefficient continuously from a real torus function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AVenhance.Infra.Classical.classicalComplexFourierCoeffCLM_apply (k : Fin 2 → ℤ) (v : ↥Parabolic.FourierGalerkin.ScalarTorusL2) : (classicalComplexFourierCoeffCLM k) v = UnitAddTorus.mFourierCoeff (↑↑(classicalRealToComplexTorusCLM v)) k

noncomputable def AVenhance.Infra.Classical.classicalGalerkinLimitFourierCoeffPath (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (k : Fin 2 → ℤ) : C(↑(Set.Icc 0 1), ℂ)

Fourier coefficient path of the Galerkin limit.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalRealToComplexTorusCLM_norm_le (v : ↥Parabolic.FourierGalerkin.ScalarTorusL2) : ‖classicalRealToComplexTorusCLM v‖ ≤ ‖v‖

theorem AVenhance.Infra.Classical.GalerkinSmoothLimit.classicalPeriodicToTorusL2_fourierCoeff_eq {f : Homogenization.Vec 2 → ℂ} (hf : Continuous f) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (↑↑(Torus.periodicToTorusL2 f hf)) k = Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Classical.classicalComplexFourierCoeffCLM_projection (N : ℕ) {f : Parabolic.FourierGalerkin.Torus → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (k : Fin 2 → ℤ) (hk : Parabolic.FourierGalerkin.frequencyPair k ∈ Parabolic.FourierGalerkin.symmetricFrequencyBox N) : (classicalComplexFourierCoeffCLM k) ((Parabolic.FourierGalerkin.realFourierScalarMap N) (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) f)) = UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(f x)) k

Fourier coefficients in a finite real Galerkin projection agree with those of the projected datum at every frequency contained in the cutoff.

theorem AVenhance.Infra.Classical.GalerkinSmoothLimit.classicalGalerkinWordFourierCoeff_eq_smooth (N : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (k : Fin 2 → ℤ) : (classicalComplexFourierCoeffCLM k) ((Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N w) c)) = Torus.smoothFourierCoeff (Torus.realToComplex (classicalWordDerivative w (realFourierModeAmbientExpansion N c))) k

theorem AVenhance.Infra.Classical.classicalGalerkinWordFourierCoeff_derivative (N : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) (k : Fin 2 → ℤ) : (classicalComplexFourierCoeffCLM k) ((Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N (i :: w)) c)) = 2 * ↑Real.pi * Complex.I * ↑(k i) * (classicalComplexFourierCoeffCLM k) ((Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N w) c))

noncomputable def AVenhance.Infra.Classical.classicalGalerkinWordLimitFourierCoeffPath (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) (k : Fin 2 → ℤ) : C(↑(Set.Icc 0 1), ℂ)

Fourier coefficient path of a spatial derivative word of the Galerkin limit.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinWordFourierCoeff_eval_tendsto (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) (k : Fin 2 → ℤ) (t : ↑(Set.Icc 0 1)) : Filter.Tendsto (fun (N : ℕ) => (classicalComplexFourierCoeffCLM k) ((classicalGalerkinWordScalarPath φ hφ κ hκ F hF θ₀ hθ₀ w N) t)) Filter.atTop (nhds ((classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w k) t))

theorem AVenhance.Infra.Classical.classicalGalerkinWordLimitFourierCoeff_derivative (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) (i : Fin 2) (k : Fin 2 → ℤ) (t : ↑(Set.Icc 0 1)) : (classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per (i :: w) k) t = 2 * ↑Real.pi * Complex.I * ↑(k i) * (classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w k) t