Strong Cauchy convergence of nested smooth Fourier Galerkin paths.

@[instance_reducible]

noncomputable def classicalCauchyMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalCauchyMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalCauchyProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.LinearIntegralSolution.continuousLinearMap_transform_between {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {A : ℝ → E →L[ℝ] E} {B : ℝ → F →L[ℝ] F} {f y : ℝ → E} {y₀ : E} {a b : ℝ} (hab : a ≤ b) (hy : ODE.IsLinearIntegralSolution A f y₀ a b y) (hRhs : IntervalIntegrable (ODE.linearRhs A f y) MeasureTheory.volume a b) (L : E →L[ℝ] F) : ODE.IsLinearIntegralSolution B (fun (t : ℝ) => L (f t) + L ((A t) (y t)) - (B t) (L (y t))) (L y₀) a b fun (t : ℝ) => L (y t)

A continuous linear map sends an integral solution to the target equation with the exact cross-space operator commutator in its source.

theorem AVenhance.Infra.Classical.LinearIntegralSolution.sub {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : ℝ → E →L[ℝ] E} {f g y z : ℝ → E} {y₀ z₀ : E} {a b : ℝ} (hab : a ≤ b) (hy : ODE.IsLinearIntegralSolution A f y₀ a b y) (hz : ODE.IsLinearIntegralSolution A g z₀ a b z) (hIy : IntervalIntegrable (ODE.linearRhs A f y) MeasureTheory.volume a b) (hIz : IntervalIntegrable (ODE.linearRhs A g z) MeasureTheory.volume a b) : ODE.IsLinearIntegralSolution A (fun (t : ℝ) => f t - g t) (y₀ - z₀) a b fun (t : ℝ) => y t - z t

The difference of two solutions for one linear operator solves the same equation with the difference source.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinLiftLinearMap {M N : ℕ} (hMN : M ≤ N) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M) →ₗ[ℝ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The zero-extension map on nested real Fourier coefficient spaces.

Equations

• AVenhance.Infra.Classical.classicalGalerkinLiftLinearMap hMN = { toFun := AVenhance.Infra.Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def AVenhance.Infra.Classical.classicalGalerkinLiftCLM {M N : ℕ} (hMN : M ≤ N) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M) →L[ℝ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The continuous zero-extension between nested Fourier coefficient spaces.

Equations

• AVenhance.Infra.Classical.classicalGalerkinLiftCLM hMN = LinearMap.toContinuousLinearMap (AVenhance.Infra.Classical.classicalGalerkinLiftLinearMap hMN)

@[simp]

theorem AVenhance.Infra.Classical.classicalGalerkinLiftCLM_apply {M N : ℕ} (hMN : M ≤ N) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)) : (classicalGalerkinLiftCLM hMN) c = Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN c

theorem AVenhance.Infra.Classical.classicalGalerkin_projection_lift_expansion {M N : ℕ} (hMN : M ≤ N) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)) : Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Parabolic.FourierGalerkin.modeExpansion (Parabolic.FourierGalerkin.RealFourierDimension M) (Parabolic.FourierGalerkin.realFourierModeFin M) c) = Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN c

Projecting a finite synthesis from a smaller cutoff into a larger one recovers its zero-extended coefficient vector.

theorem AVenhance.Infra.Classical.classicalGalerkinAmbientExpansion_lift {M N : ℕ} (hMN : M ≤ N) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)) : realFourierModeAmbientExpansion N (Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN c) = realFourierModeAmbientExpansion M c

The ambient finite Fourier synthesis is unchanged when its coefficients are zero-extended.

theorem AVenhance.Infra.Classical.classicalGalerkin_laplacian_projection_lift {M N : ℕ} (hMN : M ≤ N) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)) : Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => spaceLap (realFourierModeAmbientExpansion M c) x) = Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension M) (Parabolic.FourierGalerkin.realFourierModeFin M) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => spaceLap (realFourierModeAmbientExpansion M c) x))

The Laplacian preserves every finite Fourier synthesis range, so its Galerkin coefficient vector is compatible with zero extension to a larger cutoff.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinProjectionTail {M N : ℕ} (hMN : M ≤ N) (f : Homogenization.Vec 2 → ℝ) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The coefficient tail between two nested real Fourier cutoffs.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinProjectionTail_add {M N : ℕ} (hMN : M ≤ N) {f g : Homogenization.Vec 2 → ℝ} (hf : MeasureTheory.MemLp (Torus.periodicToTorus f) 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp (Torus.periodicToTorus g) 2 MeasureTheory.volume) : (classicalGalerkinProjectionTail hMN fun (x : Homogenization.Vec 2) => f x + g x) = classicalGalerkinProjectionTail hMN f + classicalGalerkinProjectionTail hMN g

theorem AVenhance.Infra.Classical.classicalGalerkinProjectionTail_smul {M N : ℕ} (hMN : M ≤ N) (a : ℝ) {f : Homogenization.Vec 2 → ℝ} (hf : MeasureTheory.MemLp (Torus.periodicToTorus f) 2 MeasureTheory.volume) : (classicalGalerkinProjectionTail hMN fun (x : Homogenization.Vec 2) => a * f x) = a • classicalGalerkinProjectionTail hMN f

theorem AVenhance.Infra.Classical.GalerkinCauchy.classicalCauchyTransport_contDiff (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

theorem AVenhance.Infra.Classical.GalerkinCauchy.classicalCauchyTransport_periodic (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : IsZ2Periodic b) (hu : IsZ2Periodic u) : IsZ2Periodic (classicalTransport b u)

theorem AVenhance.Infra.Classical.GalerkinCauchy.classicalCauchySpaceLap_contDiff {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (spaceLap u)

theorem AVenhance.Infra.Classical.GalerkinCauchy.classicalCauchySpaceLap_periodic {u : Homogenization.Vec 2 → ℝ} (hup : IsZ2Periodic u) : IsZ2Periodic (spaceLap u)

theorem AVenhance.Infra.Classical.classicalGalerkinCoefficient_rhs_eq_projectedGenerator (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : ((classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).weak.coefficient t) c + (classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).forcing t = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => F t x + (κ * spaceLap (realFourierModeAmbientExpansion N c) x - classicalTransport (streamVel φ t) (realFourierModeAmbientExpansion N c) x))

The concrete coefficient ODE right-hand side is the Fourier projection of the classical generator plus the forcing.

theorem AVenhance.Infra.Classical.classicalGalerkinNestedResidual_identity (φ : ℝ → 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 ℝ (↑⊤) θ₀) (M N : ℕ) (hMN : M ≤ N) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)) : ((classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).weak.coefficient t) (Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN c) + (classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).forcing t - Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN (((classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ M).weak.coefficient t) c + (classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ M).forcing t) = classicalGalerkinProjectionTail hMN fun (x : Homogenization.Vec 2) => F t x - classicalTransport (streamVel φ t) (realFourierModeAmbientExpansion M c) x

The nested-cutoff defect in the Galerkin vector fields is exactly the projected Fourier tail of the forcing minus transport. The diffusion part cancels because the Laplacian preserves the lower Fourier span.

theorem AVenhance.Infra.Classical.classicalSmoothDifferenceProjection_tail_norm_le (M N : ℕ) (hMN : M ≤ N) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hfp : IsZ2Periodic f) (hgp : IsZ2Periodic g) (Ef Eg : ℝ) (hEf : gradNormSq (spaceGrad f) ≤ Ef) (hEg : gradNormSq (spaceGrad g) ≤ Eg) : ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => f x - g x) - Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension M) (Parabolic.FourierGalerkin.realFourierModeFin M) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => f x - g x))‖ ≤ √((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * Ef) + √((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * Eg)

The nested real Fourier projection tail of a difference is controlled by the two separate smooth projection tails.

theorem AVenhance.Infra.Classical.classicalForcing_gradient_energy_uniform_bound (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) : ∃ (E : ℝ), 0 ≤ E ∧ ∀ t ∈ Set.Icc 0 1, gradNormSq (spaceGrad (F t)) ≤ E

The smooth forcing has a cutoff-independent Dirichlet-energy bound on the time interval.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinScalarPath (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)

The finite Fourier coefficient path viewed in scalar torus L².

Equations

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

@[simp]

theorem AVenhance.Infra.Classical.classicalGalerkinScalarPath_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 ℝ (↑⊤) θ₀) (N : ℕ) (t : ↑(Set.Icc 0 1)) : (classicalGalerkinScalarPath φ hφ κ hκ F hF θ₀ hθ₀ N) t = (Parabolic.FourierGalerkin.realFourierScalarMap N) ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)

theorem AVenhance.Infra.Classical.classicalGalerkinNestedResidual_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 ℝ (↑⊤) θ₀) (E_F E_T : ℝ) (hFenergy : ∀ t ∈ Set.Icc 0 1, gradNormSq (spaceGrad (F t)) ≤ E_F) (hTenergy : ∀ (K : ℕ), ∀ s ∈ Set.Icc 0 1, gradNormSq (spaceGrad (classicalTransport (streamVel φ s) (realFourierModeAmbientExpansion K (ODE.extendCurve classicalGalerkinNestedResidual_norm_le._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ K) s)))) ≤ E_T) (M N : ℕ) (hMN : M ≤ N) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖classicalGalerkinProjectionTail hMN fun (x : Homogenization.Vec 2) => F t x - classicalTransport (streamVel φ t) (realFourierModeAmbientExpansion M (ODE.extendCurve classicalGalerkinNestedResidual_norm_le._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ M) t)) x‖ ≤ √((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * E_F) + √((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * E_T)

The residual forcing in the nested-cutoff difference equation is uniformly small in its coefficient norm, with its size controlled by the smooth forcing and transport Dirichlet energies.

theorem AVenhance.Infra.Classical.classicalGalerkinScalarPath_nested_difference_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 θ₀) (E_F E_T : ℝ) (hFenergy : ∀ t ∈ Set.Icc 0 1, gradNormSq (spaceGrad (F t)) ≤ E_F) (hTenergy : ∀ (K : ℕ), ∀ s ∈ Set.Icc 0 1, gradNormSq (spaceGrad (classicalTransport (streamVel φ s) (realFourierModeAmbientExpansion K (ODE.extendCurve classicalGalerkinNestedResidual_norm_le._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ K) s)))) ≤ E_T) (M N : ℕ) (hMN : M ≤ N) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖(classicalGalerkinScalarPath φ hφ κ hκ F hF θ₀ hθ₀ N) ⟨t, ht⟩ - (classicalGalerkinScalarPath φ hφ κ hκ F hF θ₀ hθ₀ M) ⟨t, ht⟩‖ ≤ √((√((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * gradNormSq (spaceGrad θ₀)) ^ 2 + (√((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * E_F) + √((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * E_T)) ^ 2) * Real.exp (Parabolic.FourierGalerkin.positiveCutoffDriftConstant (streamVel φ) ⋯ ^ 2 / κ + 1))

The lifted difference of two nested classical Galerkin paths obeys the upper-cutoff energy estimate, with forcing given by the residual Fourier tail.