Smooth time coefficients of spatial Fourier cutoffs

The Fourier cutoff of a smooth periodic spacetime test is a finite Fourier sum whose scalar coefficients are smooth time tests. The coefficients are written as cell integrals so their time regularity follows by differentiation under the integral.

@[instance_reducible]

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

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.timeFourierTestCellFinite : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

def AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.timeFourierTestCellClosure : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.timeFourierTestCellClosure = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.timeFourierTestCellClosure_compact : IsCompact timeFourierTestCellClosure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.timeFourierTestCell_subset_closure : unitCube ⊆ timeFourierTestCellClosure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.timeFourierTestCell_measurable : MeasurableSet unitCube

theorem AVenhance.Infra.Parabolic.FourierGalerkin.continuous_cell_integral_of_joint {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : Continuous F) : Continuous fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, F (t, x)

A jointly continuous integrand on a bounded spatial cell has a continuous cell integral in time. The compact closure supplies a locally uniform integrable majorant.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.smoothTestTimePartial (φ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

The time derivative of a smooth spacetime test, in joint-coordinate form.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.smoothTestTimePartial φ p = (fderiv ℝ (fun (q : ℝ × Homogenization.Vec 2) => φ q.1 q.2) p) (1, 0)

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.smoothTestTimePartial_eq_deriv {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (t : ℝ) (x : Homogenization.Vec 2) : smoothTestTimePartial φ (t, x) = deriv (fun (s : ℝ) => φ s x) t

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestTimeDerivative (φ : ℝ → Homogenization.Vec 2 → ℝ) : ℝ → Homogenization.Vec 2 → ℝ

The time derivative of a smooth spacetime test, as a spacetime function.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestTimeDerivative φ t x = deriv (fun (s : ℝ) => φ s x) t

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestTimeDerivative_contDiff {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => spacetimeTestTimeDerivative φ p.1 p.2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestTimeDerivative_periodic {φ : ℝ → Homogenization.Vec 2 → ℝ} (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (t : ℝ) : IsZ2Periodic (spacetimeTestTimeDerivative φ t)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeRealFourierCoefficient (φ : ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (j : Fin (RealFourierDimension N)) (t : ℝ) : ℝ

The cell coefficient of one ambient real Fourier mode in a time-dependent test.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentFourierTest.spacetimeRealFourierCoefficient_eq_projectionCoefficient {φ : ℝ → Homogenization.Vec 2 → ℝ} (N : ℕ) (j : Fin (RealFourierDimension N)) (t : ℝ) : spacetimeRealFourierCoefficient φ N j t = (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) (Torus.periodicToTorus (φ t))).ofLp j

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeRealFourierCoefficient_deriv {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (N : ℕ) (j : Fin (RealFourierDimension N)) (t : ℝ) : deriv (spacetimeRealFourierCoefficient φ N j) t = ∫ (x : Homogenization.Vec 2) in unitCube, deriv (fun (s : ℝ) => φ s x) t * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x

Differentiation under the cell integral identifies the derivative of a time-dependent Fourier coefficient with the same coefficient of the time derivative.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeRealFourierCoefficient_deriv_eq_timeDerivativeCoefficient {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (N : ℕ) (j : Fin (RealFourierDimension N)) (t : ℝ) : deriv (spacetimeRealFourierCoefficient φ N j) t = spacetimeRealFourierCoefficient (spacetimeTestTimeDerivative φ) N j t

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeRealFourierCoefficient_contDiff_one {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (N : ℕ) (j : Fin (RealFourierDimension N)) : ContDiff ℝ 1 (spacetimeRealFourierCoefficient φ N j)

Every time coefficient of the finite spatial Fourier cutoff is continuously differentiable, and its derivative is the same coefficient applied to the time derivative of the test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestFourierCutoff_expansion {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : Section5.testFourierCutoff (φ t) N x = ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j t * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x

The time-dependent spatial cutoff is the finite Fourier sum with the smooth coefficient functions defined above.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTestFourierCutoff_timeDerivative {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : deriv (fun (s : ℝ) => Section5.testFourierCutoff (φ s) N x) t = ∑ j : Fin (RealFourierDimension N), deriv (spacetimeRealFourierCoefficient φ N j) t * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x

Differentiating a time-dependent spatial cutoff differentiates only its finite scalar coefficients.

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeRealFourierCoefficient_terminal {φ : ℝ → Homogenization.Vec 2 → ℝ} (hterminal : ∀ (x : Homogenization.Vec 2), φ 1 x = 0) (N : ℕ) (j : Fin (RealFourierDimension N)) : spacetimeRealFourierCoefficient φ N j 1 = 0

Terminal vanishing of a test is retained by every spatial Fourier coefficient.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeRealFourierCoefficient_contDiff {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (N : ℕ) (j : Fin (RealFourierDimension N)) : ContDiff ℝ (↑⊤) (spacetimeRealFourierCoefficient φ N j)

Every time coefficient of a smooth spacetime test is smooth in time. Repeated differentiation commutes with its cell Fourier integral.

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

The joint time-space Fourier cutoff of a smooth periodic spacetime test is itself smooth.