Spacetime convergence of the smooth-test Fourier cutoffs

The spatial Fourier tails from Section5.TestDensity are integrated in time by dominated convergence. These estimates are the strong L² convergence needed to pass the product weak equation from finite cutoffs to a general smooth spacetime test.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.timeTestConvergenceMeasureSpaceUnitAddCircle : 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.FourierGalerkin.timeTestConvergenceMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.timeTestConvergenceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.timeTestConvergenceProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_unitCube_measurable : MeasurableSet unitCube

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_l2Error_le_four {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (N : ℕ) : (l2NormSq fun (x : Homogenization.Vec 2) => f x - Section5.testFourierCutoff f N x) ≤ 4 * l2NormSq f

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_l2Energy_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : Continuous fun (t : ℝ) => l2NormSq (φ t)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.spacetimeTestValueCutoff_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) : Continuous fun (p : ℝ × Homogenization.Vec 2) => Section5.testFourierCutoff (φ p.1) N p.2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.spacetimeTestValueCutoff_error_energy_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) : Continuous fun (t : ℝ) => l2NormSq fun (x : Homogenization.Vec 2) => φ t x - Section5.testFourierCutoff (φ t) N x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_gradientCoord_continuous {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_gradient_continuous {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) : Continuous (spaceGrad f)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_gradientError_le_four {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hperiodic : IsZ2Periodic f) (N : ℕ) : gradNormSq (spaceGrad fun (x : Homogenization.Vec 2) => f x - Section5.testFourierCutoff f N x) ≤ 4 * gradNormSq (spaceGrad f)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.spacetimeTestSpatialGradient_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ 1 fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : Continuous fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (φ p.1) p.2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.spacetimeTestFourierCutoff_contDiff_one {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) : ContDiff ℝ 1 fun (p : ℝ × Homogenization.Vec 2) => Section5.testFourierCutoff (φ p.1) N p.2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.timeTestConvergence_gradientEnergy_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : Continuous fun (t : ℝ) => gradNormSq (spaceGrad (φ t))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentTestConvergence.spacetimeTestGradientCutoff_error_energy_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) : Continuous fun (t : ℝ) => gradNormSq (spaceGrad fun (x : Homogenization.Vec 2) => φ t x - Section5.testFourierCutoff (φ t) N x)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestValueCutoff_error_integral_tendsto {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ), l2NormSq fun (x : Homogenization.Vec 2) => φ t x - Section5.testFourierCutoff (φ t) N x ∂GalerkinTimeMeasure) Filter.atTop (nhds 0)

The square-integral of the value error of the time-dependent Fourier cutoff tends to zero.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestGradientCutoff_error_integral_tendsto {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ), gradNormSq (spaceGrad fun (x : Homogenization.Vec 2) => φ t x - Section5.testFourierCutoff (φ t) N x) ∂GalerkinTimeMeasure) Filter.atTop (nhds 0)

The spacetime square-integral of the spatial-gradient error of the time-dependent Fourier cutoff tends to zero.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestTimeDerivativeCutoff_error_integral_tendsto {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) : Filter.Tendsto (fun (N : ℕ) => ∫ (t : ℝ), l2NormSq fun (x : Homogenization.Vec 2) => spacetimeTestTimeDerivative φ t x - Section5.testFourierCutoff (spacetimeTestTimeDerivative φ t) N x ∂GalerkinTimeMeasure) Filter.atTop (nhds 0)

The time derivative has the same spacetime L² Fourier-tail convergence as a smooth periodic test.