Arbitrary tests for the synchronized Galerkin limit

The finite Fourier cutoff weak identity passes to every spacetime test by the spacetime L² tail estimates and the Cauchy--Schwarz inequality on the physical cell.

@[instance_reducible]

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

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.arbitraryTestTopHolderTwo : ⊤.HolderTriple 2 2

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

def AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTestClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell used for arbitrary weak test functions.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTestClosedCell = Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

def AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTestSpatialClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_unitCube_measurable : MeasurableSet unitCube

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_timeCube_measurable : MeasurableSet timeCube

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTestClosedCell_compact : IsCompact arbitraryTestClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTestSpatialClosedCell_compact : IsCompact arbitraryTestSpatialClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.unitCube_subset_arbitraryTestSpatialClosedCell : unitCube ⊆ arbitraryTestSpatialClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.timeCube_subset_arbitraryTestClosedCell : timeCube ⊆ arbitraryTestClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_continuous_memLp_two {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_continuous_memL2On {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : Homogenization.MemL2On unitCube f

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_smoothPeriodicTestL2_ae {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : (fun (y : Torus) => ↑↑(smoothPeriodicTestL2 hψ hperiodic) y) =ᵐ[MeasureTheory.volume] Torus.periodicToTorus ψ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.spacetimeCutoff_initialClass_eq_mode_sum {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) : smoothPeriodicTestL2 ⋯ ⋯ = ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j 0 • realFourierModeL2 N j

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.timeCube_measure_eq_iterated : MeasureTheory.volume.restrict timeCube = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.arbitraryTestFiniteTimeCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.galTime_eq_Ioo_measure : GalerkinTimeMeasure = MeasureTheory.volume.restrict (Set.Ioo 0 1)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.timeCube_square_integral_eq_time_l2 {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p ^ 2 = ∫ (t : ℝ), l2NormSq fun (x : Homogenization.Vec 2) => f (t, x) ∂GalerkinTimeMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_l2_pairing_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : |∫ (x : α), f x * g x ∂μ| ≤ √(∫ (x : α), f x ^ 2 ∂μ) * √(∫ (x : α), g x ^ 2 ∂μ)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_memLp_square_integrable {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.MemLp f 2 μ) : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_memLp_vectorCoord {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => f p ^ 2) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_spacetimeGradient_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.LimitArbitraryTest.arbitraryTest_cell_coord_le_grad {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Continuous F) (i : Fin 2) : (l2NormSq fun (x : Homogenization.Vec 2) => F x i) ≤ gradNormSq F

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_timeCube_vectorEnergy_eq {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Continuous F) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (F p) = ∫ (t : ℝ), gradNormSq fun (x : Homogenization.Vec 2) => F (t, x) ∂GalerkinTimeMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_driftCoordinate_memLp (P : FrozenDriftProblem) (i : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => P.b p.1 p.2 i) ⊤ (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_driftGradient_memLp_two (P : FrozenDriftProblem) (G : ↥GradientProductTimeL2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (P.b p.1 p.2) (synchronizedGradientRepresentative G p.1 p.2)) 2 (MeasureTheory.volume.restrict timeCube)

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

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_pairing_error_tendsto_zero {g : ℝ × Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict timeCube)) (e : ℕ → ℝ × Homogenization.Vec 2 → ℝ) (he : ∀ (N : ℕ), Continuous (e N)) (henergy : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, e N p ^ 2) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, g p * e N p) Filter.atTop (nhds 0)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_product_integrable_of_memLp_two {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_spaceGrad_sub {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) : (spaceGrad fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => spaceGrad f x - spaceGrad g x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_initialCutoff_pairing_tendsto (P : FrozenDriftProblem) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) : Filter.Tendsto (fun (N : ℕ) => ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j 0 * inner ℝ P.initialTorusL2 (realFourierModeL2 N j)) Filter.atTop (nhds (∫ (x : Homogenization.Vec 2) in unitCube, P.θ₀ x * φ 0 x))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitArbitraryTest.arbitraryTest_vectorDot_pairing_integrable {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} [MeasureTheory.IsFiniteMeasure μ] (D V : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p i) 2 μ) (hV : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => V p i) 2 μ) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (D p) (V p)) μ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_arbitrary_test_cell_identity (P : FrozenDriftProblem) (σ : ℕ → ℕ) (hσ : StrictMono σ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (hUweak : ∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) (hGweak : ∀ (v : ↥GradientProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.gradientProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Gprod v))) (S : Set ℝ) (hSmeas : MeasurableSet S) (hSae : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, t ∈ S) (hS : ∀ t ∈ S, synchronizedScalarSliceGood Uprod u t) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (hterminal : ∀ (t : ℝ), 1 ≤ t → ∀ (x : Homogenization.Vec 2), φ t x = 0) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, -synchronizedScalarRepresentative Uprod u S p.1 p.2 * deriv (fun (s : ℝ) => φ s p.2) p.1 + Homogenization.vecDot (P.b p.1 p.2) (synchronizedGradientRepresentative Gprod p.1 p.2) * φ p.1 p.2 + P.κ * Homogenization.vecDot (synchronizedGradientRepresentative Gprod p.1 p.2) (spaceGrad (φ p.1) p.2) = ∫ (x : Homogenization.Vec 2) in unitCube, P.θ₀ x * φ 0 x