ShellSumScaledTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Transporting the stationary potential projection along a dilating factor map #
StationaryCarrierTransport.lean transports the stationary potential projection
along a factor map that is equivariant: Φ (x +ᵥ ω) = x +ᵥ Φ ω. The per-layer
transport of e.perturb.assumption is carried by a map that is equivariant only
after a dilation of the acting group:
Ψ (x +ᵥ ω) = (c • x) +ᵥ Ψ ω, c = 3^k,
because the layer-k field is the layer-0 field dilated by 3^{-k} (and
rescaled by 3^{γ k}), and a dilation conjugates translations rather than
commuting with them.
This module generalizes the intertwining argument to that situation. The point
is that the stationary potential subspace does not change when the acting
group is rescaled by a nonzero constant: rescaling the action rescales every
horizontal gradient by the same constant, and horizontalGradientRange is a
submodule, hence invariant under nonzero scalars. So the conclusion is
identical to the unscaled one.
Main results #
hasHorizontalGradient_of_intertwine_smul— a bounded pair of maps intertwining the two translation actions up to the dilationccarries a horizontal gradient toc •a horizontal gradient.mem_stationaryPotentialSubspace_of_intertwine_smul— hence preserves the stationary potential subspace, for everyc ≠ 0.carrierTransport_koopman_smul,carrierTransportAdj_koopman_smul— the Koopman intertwining of a dilating factor map and of its Hilbert adjoint.stationaryPotentialProjection_carrierTransport_smul,norm_stationaryPotentialProjection_carrierTransport_smul— the naturality of the projection and the equality of the two projected energies along a dilating factor map.
Horizontal gradients under a dilating intertwiner #
theorem
Algsuperdiff.Section3.Provider.Corrector.hasHorizontalGradient_of_intertwine_smul
{d : ℕ}
{Ω : Type u_1}
{Ω' : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
[AddAction (HCPolySupport.Vec d) Ω]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ]
[AddAction (HCPolySupport.Vec d) Ω']
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω']
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω' ν]
{c : ℝ}
{Sscal : ↥(Probability.Stationary.ScalarL2 μ) →L[ℝ] ↥(Probability.Stationary.ScalarL2 ν)}
{Svec : ↥(Probability.Stationary.VectorL2 d μ) →L[ℝ] ↥(Probability.Stationary.VectorL2 d ν)}
(hcomm :
∀ (x : HCPolySupport.Vec d) (φ : ↥(Probability.Stationary.ScalarL2 μ)),
Sscal ((Probability.Stationary.koopman (c • x)) φ) = (Probability.Stationary.koopman x) (Sscal φ))
(hcoord :
∀ (i : Fin d) (F : ↥(Probability.Stationary.VectorL2 d μ)),
(Probability.Stationary.vectorL2Coord i) (Svec F) = Sscal ((Probability.Stationary.vectorL2Coord i) F))
{φ : ↥(Probability.Stationary.ScalarL2 μ)}
{F : ↥(Probability.Stationary.VectorL2 d μ)}
(hφ : Probability.Stationary.HasHorizontalGradient φ F)
:
Probability.Stationary.HasHorizontalGradient (Sscal φ) (c • Svec F)
A dilating intertwiner carries horizontal gradients to horizontal gradients, up to the dilation factor.
theorem
Algsuperdiff.Section3.Provider.Corrector.mem_stationaryPotentialSubspace_of_intertwine_smul
{d : ℕ}
{Ω : Type u_1}
{Ω' : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
[AddAction (HCPolySupport.Vec d) Ω]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ]
[AddAction (HCPolySupport.Vec d) Ω']
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω']
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω' ν]
{c : ℝ}
(hc : c ≠ 0)
{Sscal : ↥(Probability.Stationary.ScalarL2 μ) →L[ℝ] ↥(Probability.Stationary.ScalarL2 ν)}
{Svec : ↥(Probability.Stationary.VectorL2 d μ) →L[ℝ] ↥(Probability.Stationary.VectorL2 d ν)}
(hcomm :
∀ (x : HCPolySupport.Vec d) (φ : ↥(Probability.Stationary.ScalarL2 μ)),
Sscal ((Probability.Stationary.koopman (c • x)) φ) = (Probability.Stationary.koopman x) (Sscal φ))
(hcoord :
∀ (i : Fin d) (F : ↥(Probability.Stationary.VectorL2 d μ)),
(Probability.Stationary.vectorL2Coord i) (Svec F) = Sscal ((Probability.Stationary.vectorL2Coord i) F))
{F : ↥(Probability.Stationary.VectorL2 d μ)}
(hF : F ∈ Probability.Stationary.stationaryPotentialSubspace)
:
The transport along a dilating factor map #
theorem
Algsuperdiff.Section3.Provider.Corrector.carrierTransport_koopman_smul
{d : ℕ}
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[AddAction (HCPolySupport.Vec d) Ω₁]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₁]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₁ μ₁]
[AddAction (HCPolySupport.Vec d) Ω₂]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₂]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₂ μ₂]
{E : Type u_3}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{Φ : Ω₂ → Ω₁}
{c : ℝ}
(hΦ : MeasureTheory.MeasurePreserving Φ μ₂ μ₁)
(hequiv : ∀ (x : HCPolySupport.Vec d) (ω : Ω₂), Φ (x +ᵥ ω) = c • x +ᵥ Φ ω)
(x : HCPolySupport.Vec d)
(g : ↥(MeasureTheory.Lp E 2 μ₁))
:
(carrierTransport E hΦ) ((Probability.Stationary.koopman (c • x)) g) = (Probability.Stationary.koopman x) ((carrierTransport E hΦ) g)
The transport of a dilating factor map intertwines the two Koopman families
with the group dilated by c.
theorem
Algsuperdiff.Section3.Provider.Corrector.carrierTransportAdj_koopman_smul
{d : ℕ}
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[AddAction (HCPolySupport.Vec d) Ω₁]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₁]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₁ μ₁]
[AddAction (HCPolySupport.Vec d) Ω₂]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₂]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₂ μ₂]
{E : Type u_3}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{Φ : Ω₂ → Ω₁}
{c : ℝ}
[CompleteSpace E]
(hΦ : MeasureTheory.MeasurePreserving Φ μ₂ μ₁)
(hequiv : ∀ (x : HCPolySupport.Vec d) (ω : Ω₂), Φ (x +ᵥ ω) = c • x +ᵥ Φ ω)
(y : HCPolySupport.Vec d)
(w : ↥(MeasureTheory.Lp E 2 μ₂))
:
(carrierTransportAdj E hΦ) ((Probability.Stationary.koopman y) w) = (Probability.Stationary.koopman (c • y)) ((carrierTransportAdj E hΦ) w)
The adjoint of a dilating transport intertwines the Koopman families in
the opposite direction: it turns a translation by y on Ω₂ into a
translation by c • y on Ω₁.
Both directions preserve the stationary potential subspace #
theorem
Algsuperdiff.Section3.Provider.Corrector.mem_stationaryPotentialSubspace_carrierTransport_smul
{d : ℕ}
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[AddAction (HCPolySupport.Vec d) Ω₁]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₁]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₁ μ₁]
[AddAction (HCPolySupport.Vec d) Ω₂]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₂]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₂ μ₂]
{Φ : Ω₂ → Ω₁}
{c : ℝ}
(hc : c ≠ 0)
(hΦ : MeasureTheory.MeasurePreserving Φ μ₂ μ₁)
(hequiv : ∀ (x : HCPolySupport.Vec d) (ω : Ω₂), Φ (x +ᵥ ω) = c • x +ᵥ Φ ω)
{G : ↥(Probability.Stationary.VectorL2 d μ₁)}
(hG : G ∈ Probability.Stationary.stationaryPotentialSubspace)
:
theorem
Algsuperdiff.Section3.Provider.Corrector.mem_stationaryPotentialSubspace_carrierTransportAdj_smul
{d : ℕ}
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[AddAction (HCPolySupport.Vec d) Ω₁]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₁]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₁ μ₁]
[AddAction (HCPolySupport.Vec d) Ω₂]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₂]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₂ μ₂]
{Φ : Ω₂ → Ω₁}
{c : ℝ}
(hc : c ≠ 0)
(hΦ : MeasureTheory.MeasurePreserving Φ μ₂ μ₁)
(hequiv : ∀ (x : HCPolySupport.Vec d) (ω : Ω₂), Φ (x +ᵥ ω) = c • x +ᵥ Φ ω)
{G : ↥(Probability.Stationary.VectorL2 d μ₂)}
(hG : G ∈ Probability.Stationary.stationaryPotentialSubspace)
:
Naturality of the projection along a dilating factor map #
theorem
Algsuperdiff.Section3.Provider.Corrector.stationaryPotentialProjection_carrierTransport_smul
{d : ℕ}
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[AddAction (HCPolySupport.Vec d) Ω₁]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₁]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₁ μ₁]
[AddAction (HCPolySupport.Vec d) Ω₂]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₂]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₂ μ₂]
{Φ : Ω₂ → Ω₁}
{c : ℝ}
(hc : c ≠ 0)
(hΦ : MeasureTheory.MeasurePreserving Φ μ₂ μ₁)
(hequiv : ∀ (x : HCPolySupport.Vec d) (ω : Ω₂), Φ (x +ᵥ ω) = c • x +ᵥ Φ ω)
(G : ↥(Probability.Stationary.VectorL2 d μ₁))
:
The stationary potential projection is natural under a dilating equivariant factor map. The dilation of the acting group does not change the subspace, so the conclusion is verbatim the unscaled one.
theorem
Algsuperdiff.Section3.Provider.Corrector.norm_stationaryPotentialProjection_carrierTransport_smul
{d : ℕ}
{Ω₁ : Type u_1}
{Ω₂ : Type u_2}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[AddAction (HCPolySupport.Vec d) Ω₁]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₁]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₁ μ₁]
[AddAction (HCPolySupport.Vec d) Ω₂]
[MeasurableConstVAdd (HCPolySupport.Vec d) Ω₂]
[MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω₂ μ₂]
{Φ : Ω₂ → Ω₁}
{c : ℝ}
(hc : c ≠ 0)
(hΦ : MeasureTheory.MeasurePreserving Φ μ₂ μ₁)
(hequiv : ∀ (x : HCPolySupport.Vec d) (ω : Ω₂), Φ (x +ᵥ ω) = c • x +ᵥ Φ ω)
(G : ↥(Probability.Stationary.VectorL2 d μ₁))
:
The two projected energies agree along a dilating factor map.