Product-space realization of the drift

The drift is measurable on the Euclidean space-time cell. This module transfers that measurability to time times the quotient torus, where the product-space Galerkin limits live.

@[instance_reducible]

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

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenProductSFiniteTorus : MeasureTheory.SFinite MeasureTheory.volume

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenProductTopHolderTop : ⊤.HolderTriple ⊤ ⊤

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.torusDrift_memLp_top (P : FrozenDriftProblem) : MeasureTheory.MemLp (fun (p : ℝ × Torus) => WithLp.toLp 2 (Torus.periodicToTorus (P.b p.1) p.2)) ⊤ (GalerkinTimeMeasure.prod MeasureTheory.volume)

The drift, pulled back to time times the quotient torus, is essentially bounded in the vector L² norm associated with the Euclidean two-vector norm.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.continuous_time_memLp_top {f : ℝ → ℝ} (hf : Continuous f) : MeasureTheory.MemLp f ⊤ GalerkinTimeMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProduct.realFourierExpansion_memLp_top (N : ℕ) (d : Coefficients (RealFourierDimension N)) : MeasureTheory.MemLp (modeExpansion (RealFourierDimension N) (realFourierModeFin N) d) ⊤ MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTest_memLp {η : ℝ → ℝ} (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (ψ : ↥ScalarTorusL2) : MeasureTheory.MemLp (fun (p : ℝ × Torus) => η p.1 * ↑↑ψ p.2) 2 (GalerkinTimeMeasure.prod MeasureTheory.volume)

A separated scalar product-space test belongs to the product L² space.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTestLp (η : ℝ → ℝ) (ψ : ↥ScalarTorusL2) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) : ↥ScalarProductTimeL2

The L² class of a separated scalar product-space test.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTestLp η ψ hη = MeasureTheory.MemLp.toLp (fun (p : ℝ × AVenhance.Infra.Parabolic.FourierGalerkin.Torus) => η p.1 * ↑↑ψ p.2) ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarProductLp_pairing_time (P : FrozenDriftProblem) (N : ℕ) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (ψ : ↥ScalarTorusL2) : inner ℝ (P.scalarProductLp N) (scalarProductTestLp η ψ hη) = ∫ (t : ℝ), η t * inner ℝ (P.scalarTimeFunction N t) ψ ∂GalerkinTimeMeasure

Pairing a finite scalar Galerkin sum against a separated product test agrees with the corresponding Bochner time integral of spatial L² pairings.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTest_memLp {η : ℝ → ℝ} (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (g : ↥SpatialGradientL2) : MeasureTheory.MemLp (fun (p : ℝ × Torus) => η p.1 • ↑↑g p.2) 2 (GalerkinTimeMeasure.prod MeasureTheory.volume)

A separated gradient product-space test belongs to the product L² space.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTestLp (η : ℝ → ℝ) (g : ↥SpatialGradientL2) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) : ↥GradientProductTimeL2

The L² class of a separated gradient product-space test.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTestLp η g hη = MeasureTheory.MemLp.toLp (fun (p : ℝ × AVenhance.Infra.Parabolic.FourierGalerkin.Torus) => η p.1 • ↑↑g p.2) ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientProductLp_pairing_time (P : FrozenDriftProblem) (N : ℕ) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (g : ↥SpatialGradientL2) : inner ℝ (P.gradientProductLp N) (gradientProductTestLp η g hη) = ∫ (t : ℝ), η t * inner ℝ (P.gradientTimeFunction N t) g ∂GalerkinTimeMeasure

Pairing a finite gradient Galerkin sum against a separated product test agrees with the corresponding Bochner time integral of spatial L² pairings.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.weightedDriftProductTestFunction (P : FrozenDriftProblem) (η : ℝ → ℝ) (N : ℕ) (d : Coefficients (RealFourierDimension N)) : ℝ × Torus → SpatialVector

The bounded drift multiplied by a smooth finite Fourier test is an admissible vector test for weak convergence of the Galerkin gradients.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.weightedDriftProductTest_memLp (P : FrozenDriftProblem) {η : ℝ → ℝ} (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (N : ℕ) (d : Coefficients (RealFourierDimension N)) : MeasureTheory.MemLp (P.weightedDriftProductTestFunction η N d) 2 (GalerkinTimeMeasure.prod MeasureTheory.volume)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.weightedDriftProductTestLp (P : FrozenDriftProblem) (η : ℝ → ℝ) (N : ℕ) (d : Coefficients (RealFourierDimension N)) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) : ↥GradientProductTimeL2

The product L² class of the bounded-drift test field.

Equations

• P.weightedDriftProductTestLp η N d hη = MeasureTheory.MemLp.toLp (P.weightedDriftProductTestFunction η N d) ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProduct.spatialVector_inner_toLp (v w : Homogenization.Vec 2) : inner ℝ (WithLp.toLp 2 v) (WithLp.toLp 2 w) = Homogenization.vecDot v w

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.weightedDriftProduct_slice_integral (P : FrozenDriftProblem) (N : ℕ) (η : ℝ → ℝ) (d : Coefficients (RealFourierDimension N)) (t : ℝ) : ∫ (x : Torus), inner ℝ (P.gradientProductFunction N (t, x)) (P.weightedDriftProductTestFunction η N d (t, x)) = η t * realFourierDriftBilinearForm N (fun (s : ℝ) => Torus.periodicToTorus (P.b s)) t (productExtendedCoefficients P N t) d

At each time, the spatial pairing of a finite gradient with the drift test is the concrete finite drift bilinear form.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientProductLp_weightedDrift_pairing_time (P : FrozenDriftProblem) (N : ℕ) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (d : Coefficients (RealFourierDimension N)) : inner ℝ (P.gradientProductLp N) (P.weightedDriftProductTestLp η N d hη) = ∫ (t : ℝ), η t * realFourierDriftBilinearForm N (fun (s : ℝ) => Torus.periodicToTorus (P.b s)) t (productExtendedCoefficients P N t) d ∂GalerkinTimeMeasure

The gradient product pairing with the bounded-drift test field equals the time integral of the concrete finite drift form.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.weightedDriftProduct_time_integrable (P : FrozenDriftProblem) (N : ℕ) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (d : Coefficients (RealFourierDimension N)) : MeasureTheory.Integrable (fun (t : ℝ) => η t * realFourierDriftBilinearForm N (fun (s : ℝ) => Torus.periodicToTorus (P.b s)) t (productExtendedCoefficients P N t) d) GalerkinTimeMeasure

The time-dependent finite drift pairing is integrable, by product-space L² integrability and Fubini.