Almost-every-time weak derivative slices

Separated tests identify the spatial derivative of the synchronized product limit on almost every time slice. The first step below rewrites product-space pairings as iterated spatial pairings.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.weakSlicesMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.weakSlicesMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakSlicesMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

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

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

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

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

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

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTimeL2_pairing_iterated (G : ↥GradientProductTimeL2) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (g : ↥SpatialGradientL2) : MeasureTheory.Integrable (fun (t : ℝ) => η t * ∫ (x : Torus), inner ℝ (↑↑G (t, x)) (↑↑g x)) GalerkinTimeMeasure ∧ inner ℝ G (gradientProductTestLp η g hη) = ∫ (t : ℝ), η t * ∫ (x : Torus), inner ℝ (↑↑G (t, x)) (↑↑g x) ∂GalerkinTimeMeasure

Pairing a product-space gradient against a separated test is the time integral of its spatial slice pairing.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ae_eq_zero_of_all_top_pairings {f : ℝ → ℝ} (hfMeas : MeasureTheory.AEStronglyMeasurable f GalerkinTimeMeasure) (hfInt : MeasureTheory.Integrable f GalerkinTimeMeasure) (hzero : ∀ (η : ℝ → ℝ), MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure → ∫ (t : ℝ), η t * f t ∂GalerkinTimeMeasure = 0) : f =ᵐ[GalerkinTimeMeasure] 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTimeL2_pairing_iterated (U : ↥ScalarProductTimeL2) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (v : ↥ScalarTorusL2) : MeasureTheory.Integrable (fun (t : ℝ) => η t * ∫ (x : Torus), inner ℝ (↑↑U (t, x)) (↑↑v x)) GalerkinTimeMeasure ∧ inner ℝ U (scalarProductTestLp η v hη) = ∫ (t : ℝ), η t * ∫ (x : Torus), inner ℝ (↑↑U (t, x)) (↑↑v x) ∂GalerkinTimeMeasure

Pairing a product-space scalar against a separated test is the time integral of its spatial slice pairing.

def AVenhance.Infra.Parabolic.FourierGalerkin.clampTimeToUnit : ℝ → ↑(Set.Icc 0 1)

The scalar product limit agrees on almost every time slice with the weakly continuous path, when paired against any fixed spatial L² test.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.clampTimeToUnit t = ⟨min (max t 0) 1, ⋯⟩

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakSlices.clampTimeToUnit_continuous : Continuous clampTimeToUnit

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakSlices.clampTimeToUnit_eq {t : ℝ} (ht : t ∈ Set.Ioc 0 1) : clampTimeToUnit t = ⟨t, ⋯⟩

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_scalar_slice_pairing_ae (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (hPathWeak : ∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) (hUweak : ∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) (hUcont : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) (v : ↥ScalarTorusL2) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, ∫ (x : Torus), inner ℝ (↑↑Uprod (t, x)) (↑↑v x) = inner ℝ (u (clampTimeToUnit t)) v

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTimeL2_memLp_sections (U : ↥ScalarProductTimeL2) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, MeasureTheory.MemLp (fun (x : Torus) => ↑↑U (t, x)) 2 MeasureTheory.volume

For almost every time, a product-space scalar L² class has an L² spatial slice.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTimeL2Slice (U : ↥ScalarProductTimeL2) (t : ℝ) : ↥ScalarTorusL2

Choose the spatial L² class represented by a product-space scalar section, with zero as a total value on the exceptional times where that section is not in L².

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarProductTimeL2_slice_coeFn (U : ↥ScalarProductTimeL2) (t : ℝ) (h : MeasureTheory.MemLp (fun (x : Torus) => ↑↑U (t, x)) 2 MeasureTheory.volume) : (fun (x : Torus) => ↑↑(scalarProductTimeL2Slice U t) x) =ᵐ[MeasureTheory.volume] fun (x : Torus) => ↑↑U (t, x)

The selected scalar section agrees a.e. in space with the product representative at every time whose section is in L².

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTimeL2_memLp_sections (G : ↥GradientProductTimeL2) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, MeasureTheory.MemLp (fun (x : Torus) => ↑↑G (t, x)) 2 MeasureTheory.volume

For almost every time, a product-space vector-gradient L² class has an L² spatial slice.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTimeL2Slice (G : ↥GradientProductTimeL2) (t : ℝ) : ↥SpatialGradientL2

Choose the spatial vector-valued L² class represented by a product-gradient section, with zero as a total value at exceptional times.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.gradientProductTimeL2_slice_coeFn (G : ↥GradientProductTimeL2) (t : ℝ) (h : MeasureTheory.MemLp (fun (x : Torus) => ↑↑G (t, x)) 2 MeasureTheory.volume) : (fun (x : Torus) => ↑↑(gradientProductTimeL2Slice G t) x) =ᵐ[MeasureTheory.volume] fun (x : Torus) => ↑↑G (t, x)

The selected vector section agrees almost everywhere in space with the product representative whenever the section belongs to L².

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_scalar_slice_eq_path_ae (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (hPathWeak : ∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) (hUweak : ∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) (hUcont : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) : (fun (t : ℝ) => scalarProductTimeL2Slice Uprod t) =ᵐ[GalerkinTimeMeasure] fun (t : ℝ) => u (clampTimeToUnit t)

The product scalar limit and the weak path have the same spatial L² slice for almost every time.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_spatial_derivative_ae (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (hPathWeak : ∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) (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))) (hUcont : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) (hUbound : ∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ P.scalarBound) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, ∫ (x : Torus), inner ℝ (↑↑Gprod (t, x)) (↑↑((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) x) = -inner ℝ (u (clampTimeToUnit t)) (smoothPeriodicTestL2 ⋯ ⋯)

A fixed smooth periodic test satisfies the spatial weak derivative identity for almost every time slice of the synchronized scalar path and product-gradient limit.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_spatial_derivative_ae_countable (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (hPathWeak : ∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) (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))) (hUcont : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) (hUbound : ∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ P.scalarBound) {ι : Type u_1} [Countable ι] (i : Fin 2) (ψ : ι → Homogenization.Vec 2 → ℝ) (hψ : ∀ (a : ι), ContDiff ℝ (↑⊤) (ψ a)) (hperiodic : ∀ (a : ι), IsZ2Periodic (ψ a)) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, ∀ (a : ι), ∫ (x : Torus), inner ℝ (↑↑Gprod (t, x)) (↑↑((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 ⋯ ⋯)) x) = -inner ℝ (u (clampTimeToUnit t)) (smoothPeriodicTestL2 ⋯ ⋯)

A countable family of smooth periodic tests has one common full-measure set of times on which all spatial derivative pairings hold. This is the form used for the Fourier basis.