A pointwise scalar representative of the synchronized limit

The product-space scalar limit supplies good spatial representatives at almost every time. A measurable full-measure set of those slices is used to keep the physical representative measurable while retaining a defined periodic L² slice at every time.

@[instance_reducible]

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

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

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

def AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarSliceGood (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (t : ℝ) : Prop

A time is good when the scalar product representative has an L² slice equal to the weak path.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.exists_measurable_synchronizedScalarSliceGood (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (U : ↥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 ℝ U v))) (hUcont : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) : ∃ (S : Set ℝ), MeasurableSet S ∧ (∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, t ∈ S) ∧ ∀ t ∈ S, synchronizedScalarSliceGood U u t

The good scalar slices contain a measurable full-measure set of times.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarRepresentative (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) : ℝ → Homogenization.Vec 2 → ℝ

The pointwise scalar representative uses the product limit on good time slices and the weakly continuous path on the exceptional slices.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarRepresentative.synchronizedScalarRepresentative_good_slice_eq_canonical (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (hS : ∀ t ∈ S, synchronizedScalarSliceGood U u t) {t : ℝ} (ht : t ∈ S) : (fun (x : Homogenization.Vec 2) => synchronizedScalarRepresentative U u S t x) =ᵐ[MeasureTheory.volume.restrict unitCube] scalarTorusRepresentative (scalarProductTimeL2Slice U t)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarRepresentative_pointwise_clauses (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (B : ℝ) (hB : 0 ≤ B) (hS : ∀ t ∈ S, synchronizedScalarSliceGood U u t) (hbound : ∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ B) : (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (synchronizedScalarRepresentative U u S t) ∧ Homogenization.MemL2On unitCube (synchronizedScalarRepresentative U u S t)) ∧ ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, l2NormSq (synchronizedScalarRepresentative U u S t) ≤ C

Every time slice of the representative is periodic and belongs to the cell L² space; its cell norm is bounded by the path bound.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarRepresentative_memLp_timeCube (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (hSmeas : MeasurableSet S) (hSae : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, t ∈ S) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => synchronizedScalarRepresentative U u S p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube)

The representative is in the exact scalar space-time L² carrier.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarRepresentative.clampTimeToUnit_eq_of_mem_Icc {t : ℝ} (ht : t ∈ Set.Icc 0 1) : clampTimeToUnit t = ⟨t, ht⟩

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarRepresentative_pullback_ae (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (hSmeas : MeasurableSet S) (hSae : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, t ∈ S) : (fun (p : ℝ × Homogenization.Vec 2) => synchronizedScalarRepresentative U u S p.1 p.2) =ᵐ[MeasureTheory.volume.restrict timeCube] fun (p : ℝ × Homogenization.Vec 2) => ↑↑U (physicalTimeTorusMap p)

On almost every physical spacetime point, the selected scalar representative is the pullback of the synchronized product-space limit.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarRepresentative_pairing_eq_inner (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (hS : ∀ t ∈ S, synchronizedScalarSliceGood U u t) {t : ℝ} (ht : t ∈ Set.Icc 0 1) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : ∫ (x : Homogenization.Vec 2) in unitCube, synchronizedScalarRepresentative U u S t x * ψ x = inner ℝ (u ⟨t, ht⟩) (smoothPeriodicTestL2 hψ hperiodic)

Every spatial smooth periodic pairing of the selected physical representative is exactly the pairing of the weakly continuous torus path, including exceptional and endpoint times.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedScalarRepresentative_testPairing_continuous (U : ↥ScalarProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (hS : ∀ t ∈ S, synchronizedScalarSliceGood U u t) (hweakContinuous : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, synchronizedScalarRepresentative U u S t x * ψ x) (Set.Icc 0 1)

Smooth periodic spatial pairings of the selected representative are continuous on the closed time interval.