StationaryProjection

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Stationary potential projection

This file constructs the Hilbert-space realization of the stationary operator ∇ Δ⁻¹ div. The potential space is the closure of the full range of strong horizontal gradients for a real translation action; it is not a selected cylinder class or an abstract subspace parameter.

theorem Algsuperdiff.Probability.Stationary.measurePreserving_const_vadd {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (x : HCPolySupport.Vec d) : MeasureTheory.MeasurePreserving (fun (ω : Ω) => x +ᵥ ω) μ μ

A fixed stationary translation is measure-preserving. The construction only needs measurability in the field variable, not joint measurability of the translation parameter and the field.

@[reducible, inline]

abbrev Algsuperdiff.Probability.Stationary.ScalarL2 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : AddSubgroup (Ω →ₘ[μ] ℝ)

Scalar stationary square-integrable random variables.

Equations

• Algsuperdiff.Probability.Stationary.ScalarL2 μ = MeasureTheory.Lp ℝ 2 μ

@[reducible, inline]

noncomputable abbrev Algsuperdiff.Probability.Stationary.VectorL2 {Ω : Type u_1} [MeasurableSpace Ω] (d : ℕ) (μ : MeasureTheory.Measure Ω) : AddSubgroup (Ω →ₘ[μ] HCPolySupport.HilbertVec d)

Euclidean-vector-valued stationary square-integrable random variables.

Equations

• Algsuperdiff.Probability.Stationary.VectorL2 d μ = MeasureTheory.Lp (HCPolySupport.HilbertVec d) 2 μ

def Algsuperdiff.Probability.Stationary.koopman {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : HCPolySupport.Vec d) : ↥(MeasureTheory.Lp E 2 μ) →ₗᵢ[ℝ] ↥(MeasureTheory.Lp E 2 μ)

The Koopman isometry induced by a measure-preserving translation.

Equations

• Algsuperdiff.Probability.Stationary.koopman x = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x_1 : Ω) => x +ᵥ x_1) ⋯

noncomputable def Algsuperdiff.Probability.Stationary.vectorL2Coord {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (i : Fin d) : ↥(VectorL2 d μ) →L[ℝ] ↥(ScalarL2 μ)

The ith coordinate of a vector-valued L² random variable.

Equations

• Algsuperdiff.Probability.Stationary.vectorL2Coord i = ContinuousLinearMap.compLpL 2 μ (PiLp.proj 2 (fun (x : Fin d) => ℝ) i)

def Algsuperdiff.Probability.Stationary.HasHorizontalGradient {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (φ : ↥(ScalarL2 μ)) (F : ↥(VectorL2 d μ)) : Prop

F is the full strong horizontal gradient of φ.

Equations

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

theorem Algsuperdiff.Probability.Stationary.hasHorizontalGradient_zero {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] : HasHorizontalGradient 0 0

theorem Algsuperdiff.Probability.Stationary.HasHorizontalGradient.add {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {φ ψ : ↥(ScalarL2 μ)} {F G : ↥(VectorL2 d μ)} (hφ : HasHorizontalGradient φ F) (hψ : HasHorizontalGradient ψ G) : HasHorizontalGradient (φ + ψ) (F + G)

theorem Algsuperdiff.Probability.Stationary.HasHorizontalGradient.smul {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (c : ℝ) {φ : ↥(ScalarL2 μ)} {F : ↥(VectorL2 d μ)} (hφ : HasHorizontalGradient φ F) : HasHorizontalGradient (c • φ) (c • F)

def Algsuperdiff.Probability.Stationary.horizontalGradientRange {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] : Submodule ℝ ↥(VectorL2 d μ)

The linear range of all full strong horizontal gradients.

Equations

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

noncomputable def Algsuperdiff.Probability.Stationary.stationaryPotentialSubspace {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] : Submodule ℝ ↥(VectorL2 d μ)

The closed stationary potential subspace.

Equations

• Algsuperdiff.Probability.Stationary.stationaryPotentialSubspace = Algsuperdiff.Probability.Stationary.horizontalGradientRange.topologicalClosure

noncomputable def Algsuperdiff.Probability.Stationary.stationarySolenoidalSubspace {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] : Submodule ℝ ↥(VectorL2 d μ)

The stationary solenoidal subspace.

Equations

• Algsuperdiff.Probability.Stationary.stationarySolenoidalSubspace = Algsuperdiff.Probability.Stationary.stationaryPotentialSubspaceᗮ

instance Algsuperdiff.Probability.Stationary.stationaryPotentialSubspace_hasOrthogonalProjection {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] : stationaryPotentialSubspace.HasOrthogonalProjection

noncomputable def Algsuperdiff.Probability.Stationary.stationaryPotentialProjection {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] : ↥(VectorL2 d μ) →L[ℝ] ↥(VectorL2 d μ)

Orthogonal projection onto stationary potential fields.

Equations

• Algsuperdiff.Probability.Stationary.stationaryPotentialProjection = Algsuperdiff.Probability.Stationary.stationaryPotentialSubspace.starProjection

theorem Algsuperdiff.Probability.Stationary.stationaryPotentialProjection_mem {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (F : ↥(VectorL2 d μ)) : stationaryPotentialProjection F ∈ stationaryPotentialSubspace

theorem Algsuperdiff.Probability.Stationary.sub_stationaryPotentialProjection_mem_orthogonal {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (F : ↥(VectorL2 d μ)) : F - stationaryPotentialProjection F ∈ stationarySolenoidalSubspace

theorem Algsuperdiff.Probability.Stationary.eq_stationaryPotentialProjection_of_mem_of_sub_mem_orthogonal {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {F q : ↥(VectorL2 d μ)} (hq : q ∈ stationaryPotentialSubspace) (hFq : F - q ∈ stationarySolenoidalSubspace) : q = stationaryPotentialProjection F

Potential membership and the weak divergence identity characterize the stationary potential projection.

theorem Algsuperdiff.Probability.Stationary.continuous_koopman_orbit {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Ω] [R1Space Ω] [BorelSpace Ω] [ContinuousVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] (f : ↥(MeasureTheory.Lp E 2 μ)) : Continuous fun (x : HCPolySupport.Vec d) => (koopman x) f

Every Koopman orbit is strongly continuous under the standard topological hypotheses on the probability carrier and its real translation action.