Weak extraction in the scalar and gradient time-L² spaces

The positive-cutoff paths are continuous with values in their spatial Hilbert spaces. The scalar energy estimate bounds the time-L² scalar sequence, and the integrated Galerkin estimate bounds the time-L² gradient sequence. This file extracts one subsequence weakly in both spaces.

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

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

@[instance_reducible]

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

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

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.ScalarTimeL2 : AddSubgroup (ℝ →ₘ[MeasureTheory.volume.restrict (Set.Ioc 0 1)] ↥ScalarTorusL2)

Scalar L² paths on the open time interval.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.ScalarTimeL2 = MeasureTheory.Lp (↥AVenhance.Infra.Parabolic.FourierGalerkin.ScalarTorusL2) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 1))

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.GradientTimeL2 : AddSubgroup (ℝ →ₘ[MeasureTheory.volume.restrict (Set.Ioc 0 1)] ↥SpatialGradientL2)

Gradient L² paths on the open time interval.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.GradientTimeL2 = MeasureTheory.Lp (↥AVenhance.Infra.Parabolic.FourierGalerkin.SpatialGradientL2) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 1))

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeScalarSecondCountable : SecondCountableTopology ↥ScalarTorusL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeGradientSecondCountable : SecondCountableTopology ↥SpatialGradientL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeTimeMeasureSeparable : MeasureTheory.IsSeparable (MeasureTheory.volume.restrict (Set.Ioc 0 1))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeScalarTimeSecondCountable : SecondCountableTopology ↥ScalarTimeL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeGradientTimeSecondCountable : SecondCountableTopology ↥GradientTimeL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeScalarTimeSeparable : TopologicalSpace.SeparableSpace ↥ScalarTimeL2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spacetimeGradientTimeSeparable : TopologicalSpace.SeparableSpace ↥GradientTimeL2

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

Extend the finite Galerkin coefficient path constantly beyond the unit time interval.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarTimeFunction (P : FrozenDriftProblem) (N : ℕ) : ℝ → ↥ScalarTorusL2

The globally extended scalar Galerkin path, used only as an a.e. representative on (0,1).

Equations

• P.scalarTimeFunction N t = (AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap N) (AVenhance.Infra.Parabolic.FourierGalerkin.SpacetimeCompactness.extendedCoefficients P N t)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientTimeFunction (P : FrozenDriftProblem) (N : ℕ) : ℝ → ↥SpatialGradientL2

The globally extended gradient Galerkin path, used only as an a.e. representative on (0,1).

Equations

• P.gradientTimeFunction N t = (P.galerkinData N).gradient (AVenhance.Infra.Parabolic.FourierGalerkin.SpacetimeCompactness.extendedCoefficients P N t)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeFunction_continuous (P : FrozenDriftProblem) (N : ℕ) : Continuous (P.scalarTimeFunction N)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientTimeFunction_continuous (P : FrozenDriftProblem) (N : ℕ) : Continuous (P.gradientTimeFunction N)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeFunction_eq_scalarPath (P : FrozenDriftProblem) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Ioc 0 1) : P.scalarTimeFunction N t = (P.scalarPath N) ⟨t, ⋯⟩

On the physical open time interval, the globally extended product representative agrees with the chosen continuous Galerkin path.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeFunction_norm_bound (P : FrozenDriftProblem) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Ioc 0 1) : ‖P.scalarTimeFunction N t‖ ≤ P.scalarBound

theorem AVenhance.Infra.Parabolic.FourierGalerkin.SpacetimeCompactness.gradientTimeFunction_energy (P : FrozenDriftProblem) (N : ℕ) : ∫ (t : ℝ) in 0..1, ‖P.gradientTimeFunction N t‖ ^ 2 ≤ P.gradientEnergyBound

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeFunction_memLp (P : FrozenDriftProblem) (N : ℕ) : MeasureTheory.MemLp (P.scalarTimeFunction N) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 1))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientTimeFunction_memLp (P : FrozenDriftProblem) (N : ℕ) : MeasureTheory.MemLp (P.gradientTimeFunction N) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 1))

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeLp_norm_le (P : FrozenDriftProblem) (N : ℕ) : ‖MeasureTheory.MemLp.toLp (P.scalarTimeFunction N) ⋯‖ ≤ P.scalarBound

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientTimeLp_norm_sq_le (P : FrozenDriftProblem) (N : ℕ) : ‖MeasureTheory.MemLp.toLp (P.gradientTimeFunction N) ⋯‖ ^ 2 ≤ P.gradientEnergyBound

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeLp (P : FrozenDriftProblem) (N : ℕ) : ↥ScalarTimeL2

Scalar Galerkin evolution as an element of the time-L² space.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.scalarTimeLp P N = MeasureTheory.MemLp.toLp (P.scalarTimeFunction N) ⋯

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.gradientTimeLp (P : FrozenDriftProblem) (N : ℕ) : ↥GradientTimeL2

Galerkin gradient evolution as an element of the time-L² space.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.gradientTimeLp P N = MeasureTheory.MemLp.toLp (P.gradientTimeFunction N) ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.exists_weakSpacetime_subsequence (P : FrozenDriftProblem) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (u : ↥ScalarTimeL2) (g : ↥GradientTimeL2), (∀ (v : ↥ScalarTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (scalarTimeLp P (φ n)) v) Filter.atTop (nhds (inner ℝ u v))) ∧ (∀ (v : ↥GradientTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (gradientTimeLp P (φ n)) v) Filter.atTop (nhds (inner ℝ g v))) ∧ ‖u‖ ≤ P.scalarBound ∧ ‖g‖ ^ 2 ≤ P.gradientEnergyBound

Extract a common weakly convergent subsequence of the scalar and gradient time-L² Galerkin sequences. The scalar limit is bounded by the energy estimate, while the gradient limit is bounded by the integrated dissipation estimate.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.exists_simultaneous_weak_limit (P : FrozenDriftProblem) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (U : ↥ScalarTimeL2) (G : ↥GradientTimeL2), (∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) ∧ (∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (φ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) ∧ (∀ (v : ↥ScalarTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (scalarTimeLp P (φ n)) v) Filter.atTop (nhds (inner ℝ U v))) ∧ (∀ (v : ↥GradientTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (gradientTimeLp P (φ n)) v) Filter.atTop (nhds (inner ℝ G v))) ∧ (∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ P.scalarBound) ∧ u ⟨0, ⋯⟩ = P.initialTorusL2 ∧ ‖U‖ ≤ P.scalarBound ∧ ‖G‖ ^ 2 ≤ P.gradientEnergyBound

A common cutoff subsequence has weak scalar and gradient time-L² limits and a weakly continuous scalar path limit with the correct initial trace. The path extraction is applied to the selected spacetime subsequence, so all limits refer to the same sequence.