Product-space weak compactness for the explicit Galerkin sums

This file realizes the finite real Fourier paths as functions on time times the torus. Their product-space L² bounds are the same scalar and dissipation bounds used for the Bochner paths.

@[instance_reducible]

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessTwoNeTop : Fact (2 ≠ ⊤)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessOneLeTwo : Fact (1 ≤ 2)

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

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.GalerkinTimeMeasure : MeasureTheory.Measure ℝ

The physical time measure used in the product-space realization.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.GalerkinTimeMeasure = MeasureTheory.volume.restrict (Set.Ioc 0 1)

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.ScalarProductTimeL2 : AddSubgroup (ℝ × Torus →ₘ[GalerkinTimeMeasure.prod MeasureTheory.volume] ℝ)

Scalar product-space L² on (0,1) × 𝕋².

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.ScalarProductTimeL2 = MeasureTheory.Lp ℝ 2 (AVenhance.Infra.Parabolic.FourierGalerkin.GalerkinTimeMeasure.prod MeasureTheory.volume)

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.GradientProductTimeL2 : AddSubgroup (ℝ × Torus →ₘ[GalerkinTimeMeasure.prod MeasureTheory.volume] SpatialVector)

Vector-gradient product-space L² on (0,1) × 𝕋².

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessTimeSeparable : MeasureTheory.IsSeparable GalerkinTimeMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessTorusSeparable : MeasureTheory.IsSeparable MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessProductMeasureSeparable : MeasureTheory.IsSeparable (GalerkinTimeMeasure.prod MeasureTheory.volume)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessScalarSecondCountable : SecondCountableTopology ↥ScalarProductTimeL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessGradientSecondCountable : SecondCountableTopology ↥GradientProductTimeL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessScalarSeparable : TopologicalSpace.SeparableSpace ↥ScalarProductTimeL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productCompactnessGradientSeparable : TopologicalSpace.SeparableSpace ↥GradientProductTimeL2

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.coefficientComponent (P : FrozenDriftProblem) (N : ℕ) (i : Fin (RealFourierDimension N)) : ℝ → ℝ

Coordinate of the extended finite Galerkin coefficient path.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.productExtendedCoefficients (P : FrozenDriftProblem) (N : ℕ) : ℝ → Coefficients (RealFourierDimension N)

The coefficient path extended to all real times for product-space representatives.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarProductFunction (P : FrozenDriftProblem) (N : ℕ) : ℝ × Torus → ℝ

The explicit scalar Fourier sum on the product of time with the torus.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientProductFunction (P : FrozenDriftProblem) (N : ℕ) : ℝ × Torus → SpatialVector

The explicit gradient Fourier sum on the product of time with the torus.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductCompactness.coefficientComponent_continuous (P : FrozenDriftProblem) (N : ℕ) (i : Fin (RealFourierDimension N)) : Continuous (coefficientComponent P N i)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductCompactness.coefficientComponent_bound (P : FrozenDriftProblem) (N : ℕ) (i : Fin (RealFourierDimension N)) {t : ℝ} (ht : t ∈ Set.Ioc 0 1) : |coefficientComponent P N i t| ≤ P.scalarBound

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductCompactness.coefficientComponent_memLp_top (P : FrozenDriftProblem) (N : ℕ) (i : Fin (RealFourierDimension N)) : MeasureTheory.MemLp (coefficientComponent P N i) ⊤ GalerkinTimeMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductFunction_memLp (P : FrozenDriftProblem) (N : ℕ) : MeasureTheory.MemLp (P.scalarProductFunction N) 2 (GalerkinTimeMeasure.prod MeasureTheory.volume)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductFunction_memLp (P : FrozenDriftProblem) (N : ℕ) : MeasureTheory.MemLp (P.gradientProductFunction N) 2 (GalerkinTimeMeasure.prod MeasureTheory.volume)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarProductLp (P : FrozenDriftProblem) (N : ℕ) : ↥ScalarProductTimeL2

The scalar product-space equivalence class of a finite Galerkin sum.

Equations

• P.scalarProductLp N = MeasureTheory.MemLp.toLp (P.scalarProductFunction N) ⋯

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientProductLp (P : FrozenDriftProblem) (N : ℕ) : ↥GradientProductTimeL2

The gradient product-space equivalence class of a finite Galerkin sum.

Equations

• P.gradientProductLp N = MeasureTheory.MemLp.toLp (P.gradientProductFunction N) ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductCompactness.productTimeL2_norm_sq_eq_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {μ : MeasureTheory.Measure (ℝ × Torus)} {f : ℝ × Torus → E} (hf : MeasureTheory.MemLp f 2 μ) : ‖MeasureTheory.MemLp.toLp f hf‖ ^ 2 = ∫ (p : ℝ × Torus), ‖f p‖ ^ 2 ∂μ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductCompactness.timeL2_norm_sq_eq_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ℝ → E} (hf : MeasureTheory.MemLp f 2 GalerkinTimeMeasure) : ‖MeasureTheory.MemLp.toLp f hf‖ ^ 2 = ∫ (t : ℝ), ‖f t‖ ^ 2 ∂GalerkinTimeMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductFunction_slice_ae (P : FrozenDriftProblem) (N : ℕ) (t : ℝ) : (fun (x : Torus) => P.scalarProductFunction N (t, x)) =ᵐ[MeasureTheory.volume] fun (x : Torus) => ↑↑(P.scalarTimeFunction N t) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductFunction_slice_ae (P : FrozenDriftProblem) (N : ℕ) (t : ℝ) : (fun (x : Torus) => P.gradientProductFunction N (t, x)) =ᵐ[MeasureTheory.volume] fun (x : Torus) => ↑↑(P.gradientTimeFunction N t) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarProductLp_norm_sq (P : FrozenDriftProblem) (N : ℕ) : ‖P.scalarProductLp N‖ ^ 2 = ‖scalarTimeLp P N‖ ^ 2

The product-space scalar norm is the Bochner time-L² norm of the Galerkin path.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientProductLp_norm_sq (P : FrozenDriftProblem) (N : ℕ) : ‖P.gradientProductLp N‖ ^ 2 = ‖gradientTimeLp P N‖ ^ 2

The product-space gradient norm is the Bochner time-L² gradient norm.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.productLp_norm_bounds (P : FrozenDriftProblem) (N : ℕ) : ‖P.scalarProductLp N‖ ≤ P.scalarBound ∧ ‖P.gradientProductLp N‖ ^ 2 ≤ P.gradientEnergyBound

Product-space boundedness follows from the uniform scalar and dissipation estimates.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.exists_product_weak_subsequence_of_sequence (P : FrozenDriftProblem) (σ : ℕ → ℕ) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (U : ↥ScalarProductTimeL2) (G : ↥GradientProductTimeL2), (∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ (φ n))) v) Filter.atTop (nhds (inner ℝ U v))) ∧ (∀ (v : ↥GradientProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.gradientProductLp (σ (φ n))) v) Filter.atTop (nhds (inner ℝ G v))) ∧ ‖U‖ ≤ P.scalarBound ∧ ‖G‖ ^ 2 ≤ P.gradientEnergyBound

Product-space extraction along any preselected strictly increasing sequence of cutoffs. This allows the product limits to be synchronized with the weakly continuous path extraction.