Strong convergence of weak Fourier cutoffs

The finite real Fourier cutoffs of a weak path converge in spacetime L², together with their spatial gradients. This is the strong convergence needed to pass the finite coefficient energy balances to the weak path.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionConvergenceMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionConvergenceMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionConvergenceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionConvergenceProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjection_scalarTransfer_normSq {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ‖MeasureTheory.MemLp.toLp (Torus.periodicToTorus f) ⋯‖ ^ 2 = l2NormSq f

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakProjection_scalarCoefficient_eq_pairing {u : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {N : ℕ} : FourierGalerkin.modeProjectionCoefficients (FourierGalerkin.RealFourierDimension N) (FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus (u t)) = weakFourierCoefficientPath N u t

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakProjection_scalarL2_coefficients_eq_pairing {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (N : ℕ) : FourierGalerkin.realFourierProjectionCoefficients N (MeasureTheory.MemLp.toLp (Torus.periodicToTorus f) ⋯) = FourierGalerkin.modeProjectionCoefficients (FourierGalerkin.RealFourierDimension N) (FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakProjection_pythagorean (N : ℕ) (v : ↥FourierGalerkin.ScalarTorusL2) : ‖v - (FourierGalerkin.realFourierScalarMap N) (FourierGalerkin.realFourierProjectionCoefficients N v)‖ ^ 2 = ‖v‖ ^ 2 - ‖(FourierGalerkin.realFourierScalarMap N) (FourierGalerkin.realFourierProjectionCoefficients N v)‖ ^ 2

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakProjection_gradientCoefficient_eq_derivative {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} (h : IsPeriodicH1With (u t) (Du t)) (N : ℕ) (i : Fin 2) : FourierGalerkin.modeProjectionCoefficients (FourierGalerkin.RealFourierDimension N) (FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => Du t x i) = Classical.realFourierModeDerivativeCoefficients N (weakFourierCoefficientPath N u t) i

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionL2 (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : ↥FourierGalerkin.ScalarTorusL2

The cell Fourier coefficient path is the coefficient vector of the orthogonal real Fourier projection of the transferred slice.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierModeProjection (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : Homogenization.Vec 2 → ℝ

The ambient smooth Fourier polynomial associated to a weak path at one time.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionGradientL2 (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (i : Fin 2) : ↥FourierGalerkin.ScalarTorusL2

The finite projected weak-gradient component in torus L².

Equations

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierModeAmbientExpansion_periodicToTorus (N : ℕ) (c : FourierGalerkin.Coefficients (FourierGalerkin.RealFourierDimension N)) : Torus.periodicToTorus (Classical.realFourierModeAmbientExpansion N c) = FourierGalerkin.modeExpansion (FourierGalerkin.RealFourierDimension N) (FourierGalerkin.realFourierModeFin N) c

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierSynthesis_eq_expansionTransfer (N : ℕ) (c : FourierGalerkin.Coefficients (FourierGalerkin.RealFourierDimension N)) : (FourierGalerkin.realFourierScalarMap N) c = MeasureTheory.MemLp.toLp (Torus.periodicToTorus (Classical.realFourierModeAmbientExpansion N c)) ⋯

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionL2_eq_expansionTransfer (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : weakFourierProjectionL2 N u t = MeasureTheory.MemLp.toLp (Torus.periodicToTorus (weakFourierModeProjection N u t)) ⋯

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionGradientL2_eq_expansionTransfer (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (i : Fin 2) : weakFourierProjectionGradientL2 N u t i = MeasureTheory.MemLp.toLp (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => spaceGrad (weakFourierModeProjection N u t) x i) ⋯

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjection_scalarCellError_normSq {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (l2NormSq fun (x : Homogenization.Vec 2) => u t x - weakFourierModeProjection N u t x) = ‖MeasureTheory.MemLp.toLp (Torus.periodicToTorus (u t)) ⋯ - weakFourierProjectionL2 N u t‖ ^ 2

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjection_gradientCellError_normSq {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} (h : IsPeriodicH1With (u t) (Du t)) (N : ℕ) (i : Fin 2) : (l2NormSq fun (x : Homogenization.Vec 2) => Du t x i - spaceGrad (weakFourierModeProjection N u t) x i) = ‖MeasureTheory.MemLp.toLp (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => Du t x i) ⋯ - weakFourierProjectionGradientL2 N u t i‖ ^ 2

The cell L² error of a projected weak-gradient component is exactly its torus L² error.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjection_scalarCellError_eq_deficit {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (l2NormSq fun (x : Homogenization.Vec 2) => u t x - weakFourierModeProjection N u t x) = l2NormSq (u t) - ‖weakFourierProjectionL2 N u t‖ ^ 2

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjection_gradientCellError_eq_deficit {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} (h : IsPeriodicH1With (u t) (Du t)) (N : ℕ) (i : Fin 2) : (l2NormSq fun (x : Homogenization.Vec 2) => Du t x i - spaceGrad (weakFourierModeProjection N u t) x i) = (l2NormSq fun (x : Homogenization.Vec 2) => Du t x i) - ‖weakFourierProjectionGradientL2 N u t i‖ ^ 2

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionL2_tendsto {u : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hu : Homogenization.MemL2On unitCube (u t)) : Filter.Tendsto (fun (N : ℕ) => weakFourierProjectionL2 N u t) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (Torus.periodicToTorus (u t)) ⋯))

The finite weak Fourier projection converges to every L² slice in torus L².

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionGradientL2_tendsto {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} (h : IsPeriodicH1With (u t) (Du t)) (i : Fin 2) : Filter.Tendsto (fun (N : ℕ) => (FourierGalerkin.realFourierScalarMap N) (Classical.realFourierModeDerivativeCoefficients N (weakFourierCoefficientPath N u t) i)) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => Du t x i) ⋯))

The derivatives of the finite weak Fourier projections converge to the weak-gradient components in torus L² on every slice with periodic H¹ data.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierMode_smooth (N : ℕ) (i : Fin (FourierGalerkin.RealFourierDimension N)) : ContDiff ℝ (↑⊤) (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierMode_periodic (N : ℕ) (i : Fin (FourierGalerkin.RealFourierDimension N)) : IsZ2Periodic (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierCoefficientPath_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) : ContinuousOn (fun (t : ℝ) => weakFourierCoefficientPath N u t) (Set.Icc 0 1)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjectionL2_normSq_tendsto {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : Filter.Tendsto (fun (N : ℕ) => ‖weakFourierProjectionL2 N u t‖ ^ 2) Filter.atTop (nhds (l2NormSq (u t)))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjectionL2_normSq_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) : ContinuousOn (fun (t : ℝ) => ‖weakFourierProjectionL2 N u t‖ ^ 2) (Set.Icc 0 1)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierDerivativeCoefficientPath_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) (i : Fin 2) : ContinuousOn (fun (t : ℝ) => Classical.realFourierModeDerivativeCoefficients N (weakFourierCoefficientPath N u t) i) (Set.Icc 0 1)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjectionGradientL2_normSq_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) (i : Fin 2) : ContinuousOn (fun (t : ℝ) => ‖weakFourierProjectionGradientL2 N u t i‖ ^ 2) (Set.Icc 0 1)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjectionGradientL2_normSq_tendsto {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} (h : IsPeriodicH1With (u t) (Du t)) (i : Fin 2) : Filter.Tendsto (fun (M : ℕ) => ‖weakFourierProjectionGradientL2 M u t i‖ ^ 2) Filter.atTop (nhds (l2NormSq fun (x : Homogenization.Vec 2) => Du t x i))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakProjection_timeCube_measure_eq_product : MeasureTheory.volume.restrict timeCube = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakGradientComponent_l2NormSq_time_integrable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (i : Fin 2) : MeasureTheory.Integrable (fun (t : ℝ) => l2NormSq fun (x : Homogenization.Vec 2) => Du t x i) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakGradientComponent_l2NormSq_aestronglyMeasurable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (i : Fin 2) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => l2NormSq fun (x : Homogenization.Vec 2) => Du t x i) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjection_gradientComponent_time_integral_tendsto {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (i : Fin 2) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ) in Set.Ioo 0 1, (l2NormSq fun (x : Homogenization.Vec 2) => Du t x i) - ‖weakFourierProjectionGradientL2 N u t i‖ ^ 2) Filter.atTop (nhds 0)

Each projected weak-gradient component converges strongly in time L².

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjectionL2_normSq_aestronglyMeasurable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (N : ℕ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => ‖weakFourierProjectionL2 N u t‖ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakPath_l2NormSq_aestronglyMeasurable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => l2NormSq (u t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The full scalar slice norm is measurable because it is the pointwise limit of the continuous finite Fourier coefficient norms.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjection_scalarL2_time_integral_tendsto {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ) in Set.Ioo 0 1, l2NormSq (u t) - ‖weakFourierProjectionL2 N u t‖ ^ 2) Filter.atTop (nhds 0)

The scalar Fourier projection errors converge strongly in time L². The equality with the cell error is the Pythagorean identity for the finite orthogonal projection.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjection_scalarCellError_time_integral_tendsto {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ) in Set.Ioo 0 1, l2NormSq fun (x : Homogenization.Vec 2) => u t x - weakFourierModeProjection N u t x) Filter.atTop (nhds 0)

The actual cell scalar cutoff error converges in spacetime L².

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjectionConvergence.weakFourierProjection_gradientCellError_time_integral_tendsto {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) (i : Fin 2) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ) in Set.Ioo 0 1, l2NormSq fun (x : Homogenization.Vec 2) => Du t x i - spaceGrad (weakFourierModeProjection N u t) x i) Filter.atTop (nhds 0)

The actual cell weak-gradient cutoff error converges in spacetime L², componentwise.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjection_strong_H1_time_convergence {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u Du) : Filter.Tendsto (fun (N : ℕ) => (∫ (t : ℝ) in Set.Ioo 0 1, l2NormSq fun (x : Homogenization.Vec 2) => u t x - weakFourierModeProjection N u t x) + ∑ i : Fin 2, ∫ (t : ℝ) in Set.Ioo 0 1, l2NormSq fun (x : Homogenization.Vec 2) => Du t x i - spaceGrad (weakFourierModeProjection N u t) x i) Filter.atTop (nhds 0)

Real Fourier projection of a weak path converges strongly in spacetime H¹: the squared time integral of the cell value error plus both weak-gradient component errors tends to zero.