G-Invariance for Meta-Variational Principle

This file defines the symmetry group G and invariance properties for the meta-variational principle framework.

Main definitions

• DirichletAutomorphism: Automorphisms preserving Dirichlet form
• ScaleTransform: Scale transformations on multi-scale parameters
• TimeReparam: Time reparametrization
• GAction: The full symmetry group G
• Invariance predicates for various structures

Implementation notes

The group G = Aut_ℰ(X) ⋉ (Doob × Scale × Reparam) acts on all components of the meta-variational principle, preserving the main inequality FG★.

noncomputable def Frourio.spectral_penalty_term {m : ℕ+} (cfg : MultiScaleConfig m) (C_energy κ : ℝ) : ℝ

Spectral penalty term for FG★

Equations

• Frourio.spectral_penalty_term cfg C_energy κ = κ * C_energy * Frourio.spectralSymbolSupNorm cfg ^ 2

structure Frourio.FGStarConstant : Type

FG★ constant structure (simplified for G-invariance)

• C_energy : ℝ

  Energy constant from FG★ inequality

• C_energy_pos : 0 < self.C_energy

  Positivity constraint

• C_energy_nonneg : 0 ≤ self.C_energy

  Non-negativity (weaker than positivity, for compatibility)

structure Frourio.MetaEVIFlags {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) : Type

Meta EVI flags structure (simplified for G-invariance)

• fgstar_const : FGStarConstant

  FG★ constant

• lam_base : ℝ

  Base curvature parameter

• doob : DoobDegradation

  Doob transform component

• lam_eff : ℝ

  Effective rate

• lam_eff_eq : self.lam_eff = self.lam_base - 2 * self.doob.ε - spectral_penalty_term cfg self.fgstar_const.C_energy κ

  Effective rate equation

theorem Frourio.withDensity_one {X : Type u_1} [MeasurableSpace X] (ν : MeasureTheory.Measure X) : (ν.withDensity fun (x : X) => 1) = ν

Technical lemma: withDensity by constant 1 is identity. This is a standard fact in measure theory.

structure Frourio.DirichletAutomorphism {X : Type u_1} [MeasurableSpace X] : Type u_1

Automorphism of X preserving the Dirichlet form ℰ

• toFun : X → X

  The underlying measurable bijection

• invFun : X → X

  Inverse function

• left_inv : Function.LeftInverse self.invFun self.toFun

  Left inverse property

• right_inv : Function.RightInverse self.invFun self.toFun

  Right inverse property

• measurable_toFun : Measurable self.toFun

  Measurability of forward map

• measurable_invFun : Measurable self.invFun

  Measurability of inverse map

• preserves_dirichlet (Γ : CarreDuChamp X) (f g : X → ℝ) : (Γ.Γ (fun (x : X) => f (self.toFun x)) fun (x : X) => g (self.toFun x)) = fun (x : X) => Γ.Γ f g (self.toFun x)

  Dirichlet-form invariance for every CarreDuChamp Γ: Pullback by toFun commutes with Γ.

structure Frourio.ScaleTransform (m : ℕ+) : Type

Scale transformation on multi-scale parameters

• σ : ℝ

  The scaling factor σ > 0

• hσ_pos : 0 < self.σ

  Positivity constraint

def Frourio.ScaleTransform.apply {m : ℕ+} (s : ScaleTransform m) (cfg : MultiScaleConfig m) : MultiScaleConfig m

Apply scale transformation to configuration

Equations

• s.apply cfg = { α := cfg.α, τ := fun (i : Fin ↑m) => s.σ * cfg.τ i, hτ_pos := ⋯, hα_sum := ⋯, hα_bound := ⋯ }

structure Frourio.TimeReparam : Type

Time reparametrization for curves

• θ : ℝ → ℝ

  The reparametrization function θ : [0,1] → [0,1]

• mono : Monotone self.θ

  Monotone increasing

• init : self.θ 0 = 0

  Boundary conditions

• terminal : self.θ 1 = 1
• continuous : Continuous self.θ

  Continuity of the reparametrization function

structure Frourio.GAction (X : Type u_1) [MeasurableSpace X] (m : ℕ+) : Type u_1

The symmetry group G for the meta-variational principle. G = Aut_ℰ(X) ⋉ (Doob × ℝ₊ × Reparam)

• aut : DirichletAutomorphism

  Dirichlet form automorphism component

• doob_h : X → ℝ

  Doob transform component (h function)

• doob_h_pos (x : X) : 0 < self.doob_h x

  Positivity of Doob function

• scale : ScaleTransform m

  Scale transformation component

• reparam : TimeReparam

  Time reparametrization component

noncomputable def Frourio.GAction.actOnMeasure {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (g : GAction X m) (μ : MeasureTheory.Measure X) : MeasureTheory.Measure X

Action of G on measures

Equations

• g.actOnMeasure μ = (MeasureTheory.Measure.map g.aut.toFun μ).withDensity fun (x : X) => ENNReal.ofReal (g.doob_h x ^ 2)

def Frourio.GAction.actOnConfig {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (g : GAction X m) (cfg : MultiScaleConfig m) : MultiScaleConfig m

Action of G on multi-scale configuration

Equations

• g.actOnConfig cfg = g.scale.apply cfg

def Frourio.entropy_G_invariant {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (Ent : MeasureTheory.Measure X → ℝ) : Prop

Invariance of entropy under G-action (up to additive constant)

Equations

• Frourio.entropy_G_invariant Ent = ∀ (g : Frourio.GAction X m) (ρ : MeasureTheory.Measure X), ∃ (c : ℝ), Ent (g.actOnMeasure ρ) = Ent ρ + c

def Frourio.dm_G_invariant {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (H : HeatSemigroup X) (Γ : CarreDuChamp X) : Prop

Invariance of modified distance under G-action

Equations

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

def Frourio.multiScaleDiff_G_invariant {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (H : HeatSemigroup X) : Prop

Invariance of multi-scale difference operator under pullback

Equations

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

theorem Frourio.spectralSymbol_scale_invariant {m : ℕ+} (cfg : MultiScaleConfig m) (s : ScaleTransform m) : spectralSymbolSupNorm (s.apply cfg) = spectralSymbolSupNorm cfg

Scale invariance of spectral symbol sup-norm. Under scale transformation τ ↦ στ with spectral variable λ ↦ λ/σ, the sup-norm ‖ψ_m‖_∞ is exactly preserved.

noncomputable def Frourio.pushforward {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (f : X → Y) (_hf : Measurable f) (μ : MeasureTheory.Measure X) : MeasureTheory.Measure Y

Pushforward of a measure by a measurable function

Equations

• Frourio.pushforward f _hf μ = MeasureTheory.Measure.map f μ

def Frourio.pullback {X : Type u_1} {Y : Type u_2} (f : X → Y) (φ : Y → ℝ) : X → ℝ

Pullback of a function by a measurable function

Equations

• Frourio.pullback f φ = φ ∘ f

theorem Frourio.entropy_pushforward_invariant {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (f : X → Y) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.SigmaFinite ν] (h_preserve : MeasureTheory.Measure.map f μ = ν) : InformationTheory.klDiv (MeasureTheory.Measure.map f μ) ν = 0

Entropy is invariant under pushforward by measure-preserving maps

theorem Frourio.dm_pullback_pushforward_compatible {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (g : DirichletAutomorphism) (h_inv : dm_G_invariant H Γ) (ρ₀ ρ₁ : MeasureTheory.Measure X) : dm H cfg Γ κ (pushforward g.toFun ⋯ μ) (pushforward g.toFun ⋯ ρ₀) (pushforward g.toFun ⋯ ρ₁) = dm H cfg Γ κ μ ρ₀ ρ₁

Distance compatibility under pullback/pushforward

theorem Frourio.carre_du_champ_pullback {X : Type u_1} [MeasurableSpace X] (Γ : CarreDuChamp X) (g : DirichletAutomorphism) (φ ψ : X → ℝ) : Γ.Γ (pullback g.toFun φ) (pullback g.toFun ψ) = pullback g.toFun (Γ.Γ φ ψ)

Carré du Champ operator compatibility with pullback

structure Frourio.EntropyWithTransforms (X : Type u_1) [MeasurableSpace X] : Type u_1

Entropy functional with pushforward/pullback structure

• μ : MeasureTheory.Measure X

  Base measure

• Ent : MeasureTheory.Measure X → ENNReal

  Entropy relative to base measure

• pushforward_compat (f : X → X) (_hf : Measurable f) : self.Ent (MeasureTheory.Measure.map f self.μ) = 0

  Pushforward compatibility

• pullback_integrable (φ : X → ℝ) (g : DirichletAutomorphism) : MeasureTheory.Integrable φ self.μ → MeasureTheory.Integrable (pullback g.toFun φ) self.μ

  Pullback of test functions preserves integrability

structure Frourio.ModifiedDistanceWithTransforms {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) : Type u_1

Modified distance with pullback/pushforward structure

• μ : MeasureTheory.Measure X

  Base measure

• d_m : MeasureTheory.Measure X → MeasureTheory.Measure X → ℝ

  The modified distance function

• pushforward_preserves (g : DirichletAutomorphism) (ρ₀ ρ₁ : MeasureTheory.Measure X) : self.d_m (pushforward g.toFun ⋯ ρ₀) (pushforward g.toFun ⋯ ρ₁) = self.d_m ρ₀ ρ₁

  Pushforward preserves distance

• pullback_velocity : DirichletAutomorphism → (X → ℝ) → X → ℝ

  Pullback of velocity potentials

theorem Frourio.entropy_transform_formula {X : Type u_1} [MeasurableSpace X] (μ ρ : MeasureTheory.Measure X) (g : DirichletAutomorphism) (h : X → ℝ) (h_inv : InformationTheory.klDiv ((pushforward g.toFun ⋯ ρ).withDensity fun (x : X) => ENNReal.ofReal (h x ^ 2)) ((pushforward g.toFun ⋯ μ).withDensity fun (x : X) => ENNReal.ofReal (h x ^ 2)) = InformationTheory.klDiv ρ μ) : InformationTheory.klDiv ((pushforward g.toFun ⋯ ρ).withDensity fun (x : X) => ENNReal.ofReal (h x ^ 2)) ((pushforward g.toFun ⋯ μ).withDensity fun (x : X) => ENNReal.ofReal (h x ^ 2)) = InformationTheory.klDiv ρ μ

Theorem: Entropy transformation under pullback/pushforward

theorem Frourio.dm_transform_formula {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (g : DirichletAutomorphism) (s : ScaleTransform m) (h_inv : dm_G_invariant H Γ) (hscale : ∀ (μ ρ₀ ρ₁ : MeasureTheory.Measure X), dm H (s.apply cfg) Γ (κ / s.σ) μ ρ₀ ρ₁ = s.σ * dm H cfg Γ κ μ ρ₀ ρ₁) (ρ₀ ρ₁ : MeasureTheory.Measure X) : dm H (s.apply cfg) Γ (κ / s.σ) (pushforward g.toFun ⋯ μ) (pushforward g.toFun ⋯ ρ₀) (pushforward g.toFun ⋯ ρ₁) = s.σ * dm H cfg Γ κ μ ρ₀ ρ₁

Distance formula under pullback/pushforward

theorem Frourio.pullback_preserves_L2 {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (g : DirichletAutomorphism) (φ : X → ℝ) (h_change : ∀ (f : X → ℝ), MeasureTheory.MemLp f 2 (pushforward g.toFun ⋯ μ) ↔ MeasureTheory.MemLp (pullback g.toFun f) 2 μ) : MeasureTheory.MemLp φ 2 (pushforward g.toFun ⋯ μ) ↔ MeasureTheory.MemLp (pullback g.toFun φ) 2 μ

Pullback preserves L² integrability

theorem Frourio.meta_variational_G_invariant {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (flags : MetaEVIFlags H cfg Γ κ μ) (g : GAction X m) : ∃ (transformed_flags : MetaEVIFlags H (g.actOnConfig cfg) Γ κ (g.actOnMeasure μ)), transformed_flags.lam_eff = transformed_flags.lam_base - 2 * transformed_flags.doob.ε - spectral_penalty_term (g.actOnConfig cfg) transformed_flags.fgstar_const.C_energy κ

Main theorem: Complete G-invariance of the meta-variational principle

theorem Frourio.FGStar_G_invariant {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (cfg : MultiScaleConfig m) (lam : ℝ) (doob : DoobDegradation) (κ C : ℝ) (g : GAction X m) : doob.degraded_lambda lam - κ * C * spectralSymbolSupNorm (g.actOnConfig cfg) ^ 2 = doob.degraded_lambda lam - κ * C * spectralSymbolSupNorm cfg ^ 2

Main G-invariance for FG★ (effective rate). If the Doob degradation amount ε is fixed (encoded in doob : DoobDegradation), then the effective rate λ_eff = (λ - 2ε) - κ C ‖ψ_m‖_∞^2 is invariant under the G-action components (Dirichlet automorphism, Doob, scale, reparam).

def Frourio.GAction.comp {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (g₁ g₂ : GAction X m) : GAction X m

Composition of G-actions forms a group structure

Equations

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

def Frourio.GAction.id {X : Type u_1} [MeasurableSpace X] (m : ℕ+) : GAction X m

Identity element of G-action

Equations

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

theorem Frourio.GAction.id_actOnMeasure {X : Type u_1} [MeasurableSpace X] (m : ℕ+) (μ : MeasureTheory.Measure X) : (id m).actOnMeasure μ = μ

Identity action on measures: doing nothing leaves the measure unchanged.

theorem Frourio.GAction.id_actOnConfig {X : Type u_1} [MeasurableSpace X] (m : ℕ+) (cfg : MultiScaleConfig m) : (id m).actOnConfig cfg = cfg

Identity action on configurations: parameters remain unchanged.

theorem Frourio.entropy_aut_invariant {X : Type u_1} [MeasurableSpace X] {m : ℕ+} (Ent : MeasureTheory.Measure X → ℝ) (aut : DirichletAutomorphism) (μ : MeasureTheory.Measure X) : entropy_G_invariant Ent → ∃ (c : ℝ), Ent (MeasureTheory.Measure.map aut.toFun μ) = Ent μ + c

Invariance of entropy under Dirichlet automorphism. The key observation is that when Doob h ≡ 1, the measure transformation reduces to a simple pushforward.

theorem Frourio.dm_scale_transform {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (s : ScaleTransform m) (ρ₀ ρ₁ : MeasureTheory.Measure X) (hscale : dm H (s.apply cfg) Γ (κ / s.σ) μ ρ₀ ρ₁ = s.σ * dm H cfg Γ κ μ ρ₀ ρ₁) : dm H (s.apply cfg) Γ (κ / s.σ) μ ρ₀ ρ₁ = s.σ * dm H cfg Γ κ μ ρ₀ ρ₁

Scale transformation law for dm. Under scale transformation τ ↦ στ, the modified distance transforms as: dm(στ) = σ · dm(τ) when κ is scaled appropriately.

theorem Frourio.dm_G_scale_invariant {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (g : GAction X m) (ρ₀ ρ₁ : MeasureTheory.Measure X) : dm_G_invariant H Γ → dm H (g.actOnConfig cfg) Γ κ (g.actOnMeasure μ) (g.actOnMeasure ρ₀) (g.actOnMeasure ρ₁) = dm H cfg Γ κ μ ρ₀ ρ₁

Invariance of dm under full G-action with scale component. When all components (measures and parameters) are transformed consistently, the distance is preserved.

theorem Frourio.meta_principle_G_invariant {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (Ent : MeasureTheory.Measure X → ℝ) (lam : ℝ) (doob : DoobDegradation) (g : GAction X m) : entropy_G_invariant Ent → dm_G_invariant H Γ → multiScaleDiff_G_invariant H → ∃ (lam' : ℝ) (doob' : DoobDegradation), lam' - 2 * doob'.ε - κ * spectralSymbolSupNorm (g.actOnConfig cfg) ^ 2 = lam - 2 * doob.ε - κ * spectralSymbolSupNorm cfg ^ 2

Main theorem: Full G-invariance of meta-variational principle

theorem Frourio.lam_eff_G_invariant {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (cfg : MultiScaleConfig m) (κ C lam : ℝ) (doob : DoobDegradation) (g : GAction X m) : ∃ (doob' : DoobDegradation), doob'.degraded_lambda lam - κ * C * spectralSymbolSupNorm (g.actOnConfig cfg) ^ 2 = doob.degraded_lambda lam - κ * C * spectralSymbolSupNorm cfg ^ 2

Corollary: The effective rate λ_eff is G-invariant up to Doob composition