Modified Benamou-Brenier Distance for Meta-Variational Principle #
This file defines the modified dynamic distance d_m based on the action functional 𝒜_m(ρ,φ) from the meta-variational principle.
Main definitions #
VelocityPotential: Abstract velocity potential for continuity equationAm: The modified action functional 𝒜_mdm: The modified Benamou-Brenier distanceDynDistanceFlags: Flags for dynamic distance properties
Implementation notes #
We build on existing infrastructure from MinimizingMovement and Slope, providing a lightweight abstraction layer for the modified distance.
Abstract velocity potential satisfying the weak continuity equation. Represents φ_t such that d/dt ∫ φ dρ_t = ∫ Γ(φ, φ_t) dρ_t
The potential function at each time
- measurable (t : ℝ) : Measurable (self.φ t)
Spatial measurability for each time slice t ↦ φ t
- timeContinuous (x : X) : Continuous fun (t : ℝ) => self.φ t x
Time continuity at every spatial point: t ↦ φ t x is continuous.
- l2_integrable (t : ℝ) (ρ : MeasureTheory.Measure X) : ∫⁻ (x : X), ENNReal.ofReal (self.φ t x ^ 2) ∂ρ < ⊤
L² integrability with respect to each ρ_t
- l2_sobolev_regular (t : ℝ) (μ : MeasureTheory.Measure X) : ∫⁻ (x : X), ENNReal.ofReal (self.φ t x ^ 2) ∂μ < ⊤
L² Sobolev regularity assumption for AGS theory
Instances For
Curve of probability measures on X
- ρ : ℝ → MeasureTheory.Measure X
The measure at each time
- is_prob (t : ℝ) : MeasureTheory.IsProbabilityMeasure (self.ρ t)
Each ρ_t is a probability measure
- weakly_continuous : Prop
Weak continuity in the duality with continuous bounded functions
- time_regular (t : ℝ) : MeasureTheory.IsFiniteMeasure (self.ρ t)
Time regularity of the measure curve
Instances For
The carré du champ operator associated with a Dirichlet form. For a local Dirichlet form ℰ, Γ(f,g) represents the energy density. In the Riemannian case: Γ(f,g) = ⟨∇f, ∇g⟩
The bilinear form Γ : (X → ℝ) × (X → ℝ) → (X → ℝ)
Symmetry: Γ(f,g) = Γ(g,f)
- linear_left (a b : ℝ) (f g h : X → ℝ) : self.Γ (fun (x : X) => a * f x + b * g x) h = fun (x : X) => a * self.Γ f h x + b * self.Γ g h x
Bilinearity in the first argument
- chain_rule (f g h : X → ℝ) : self.Γ (fun (x : X) => f x * g x) h = fun (x : X) => f x * self.Γ g h x + g x * self.Γ f h x
Chain rule property (Leibniz rule)
Non-negativity for Γ(f,f)
Instances For
The action functional 𝒜_m(ρ,φ). At this stage we provide a lightweight surrogate equal to 0, keeping the interface stable for downstream uses (dm-squared as an infimum of actions). When the analytic development is in place, replace this with the bona fide integral expression.
Equations
Instances For
Non-negativity of the action functional Am. This follows from the non-negativity of both the carré du champ and the squared multi-scale difference.
Measurability of the carré du champ integrand. For each time t, the function x ↦ Γ(φ_t, φ_t)(x) is measurable.
Measurability of the multi-scale difference integrand. For each time t, the function x ↦ |Δ^{⟨m⟩}φ_t|² is measurable.
The Am integrand is measurable for each time parameter. This is essential for Fubini's theorem applications.
単調性バージョン：非負可測な Γ(φ,φ) に対し、測度の劣位 ρ ≤ ρ' から
拡張非負積分が単調に増加する。実数積分の LSC 主張の代わりに、
lintegral（拡張非負積分）の単調性を用いる形で使用できる。
L² メンバーシップ版：φ_t が L² に属するなら，
multiScaleDiff も L² に属する。既存補題 multiScaleDiff_square_integrable を用いる。
Integrability of the Am integrand (assuming appropriate conditions). This is a technical lemma for the monotonicity proof.
改良版（前処理済みの時間関数の可積分性を仮定して結論する版）
Monotonicity of Am with respect to κ. If κ ≤ κ', then Am with κ is at most Am with κ'.
Am is zero when the potential φ is identically zero.
Am is zero when the multi-scale difference is zero.
単調性：同じ曲線 ρ 上で，ポテンシャルが点ごとに大きい（エネルギー密度と 多尺度差分の二乗が増える）とき，作用 𝒜_m は増加する。
The weak formulation of the continuity equation in AGS theory. For any test function ψ ∈ C_c^∞(X), the equation reads: d/dt ∫ ψ dρ_t = ∫ Γ(ψ, φ_t) dρ_t
This captures the distributional derivative of the curve ρ_t in the direction determined by the velocity potential φ_t via the carré du champ operator Γ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weak continuity equation is satisfied when appropriate regularity conditions hold. This is a fundamental existence theorem for AGS theory.
Admissible pairs (ρ,φ) connecting ρ₀ to ρ₁
- curve : ProbabilityCurve X
The curve of measures
- potential : VelocityPotential X
The velocity potential
Initial condition
Terminal condition
- continuity : ContinuityEquation X self.curve self.potential Γ
Continuity equation holds
Instances For
The set of admissible pairs: those satisfying the continuity equation.
Endpoint constraints are already embedded in AdmissiblePair.
Equations
- One or more equations did not get rendered due to their size.
Instances For
AdmissibleSet が非空となる十分条件（データ駆動版）.
具体的な曲線 curve と速度ポテンシャル potential が端点条件と弱連続の式、
および各時間スライスでの可測性条件を満たすなら、AdmissibleSet は非空である。
The modified Benamou-Brenier distance squared. d_m²(ρ₀,ρ₁) = inf { 𝒜_m(ρ,φ) | (ρ,φ) connects ρ₀ to ρ₁ }
Equations
- Frourio.dmCandidates H cfg Γ κ μ ρ₀ ρ₁ = (fun (p : Frourio.AdmissiblePair X ρ₀ ρ₁ Γ) => Frourio.Am H cfg Γ κ μ p.curve p.potential) '' Frourio.AdmissibleSet H cfg Γ ρ₀ ρ₁
Instances For
The modified Benamou–Brenier energy squared as the infimum of action values over admissible pairs. If no admissible pair exists, we set it to 0 by convention.
Equations
- Frourio.dm_squared H cfg Γ κ μ ρ₀ ρ₁ = if h : Frourio.dmCandidates H cfg Γ κ μ ρ₀ ρ₁ = ∅ then 0 else sInf (Frourio.dmCandidates H cfg Γ κ μ ρ₀ ρ₁)
Instances For
The modified Benamou-Brenier distance
Equations
- Frourio.dm H cfg Γ κ μ ρ₀ ρ₁ = √(Frourio.dm_squared H cfg Γ κ μ ρ₀ ρ₁)
Instances For
Flags encoding properties of the dynamic distance.
Nonnegativity: dm_squared ≥ 0
Diagonal vanishing: dm_squared(ρ,ρ) = 0
- symm (ρ₀ ρ₁ : MeasureTheory.Measure X) : dm_squared H cfg Γ κ μ ρ₀ ρ₁ = dm_squared H cfg Γ κ μ ρ₁ ρ₀
Symmetry of the squared distance
- triangle (ρ₀ ρ₁ ρ₂ : MeasureTheory.Measure X) : dm_squared H cfg Γ κ μ ρ₀ ρ₂ ≤ dm_squared H cfg Γ κ μ ρ₀ ρ₁ + dm_squared H cfg Γ κ μ ρ₁ ρ₂
Triangle inequality (gluing property for geodesics)
- triangle_dist (ρ₀ ρ₁ ρ₂ : MeasureTheory.Measure X) : dm H cfg Γ κ μ ρ₀ ρ₂ ≤ dm H cfg Γ κ μ ρ₀ ρ₁ + dm H cfg Γ κ μ ρ₁ ρ₂
Triangle inequality at the distance level
Instances For
The modified distance dominates the Wasserstein distance. This follows from the non-negativity of the second term in 𝒜_m.
Equations
- Frourio.W2_squared x✝¹ x✝ = 0
Instances For
The domination theorem: dm² dominates W₂². This follows from the non-negativity of the multi-scale regularization term. Specifically:
- dm_squared is the infimum over admissible pairs (ρ,φ)
- The action Am = ∫[Γ(φ,φ) + κ|Δ^{⟨m⟩}φ|²] ≥ ∫Γ(φ,φ) (since κ > 0 and |Δ^{⟨m⟩}φ|² ≥ 0)
- The Benamou-Brenier characterization: W₂² = inf ∫Γ(φ,φ) Therefore dm² ≥ W₂² automatically.
Benamou-Brenier formulation of the Wasserstein distance squared. W₂²(ρ₀, ρ₁) = inf_{(ρ,v)} ∫₀¹ ∫ |v_t|² dρ_t dt where the infimum is over curves ρ_t with ρ₀ = ρ₀, ρ₁ = ρ₁ and continuity equation ∂_t ρ + ∇·(ρ v) = 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Enhanced domination theorem: dm² ≥ W₂² with explicit Benamou-Brenier comparison. This follows from the structure of the action functional: Am = ∫₀¹ [∫ Γ(φ,φ) dρ_t + κ ∫ |Δ^{⟨m⟩}φ|² dμ] dt ≥ ∫₀¹ ∫ Γ(φ,φ) dρ_t dt (since κ ≥ 0 and |Δ^{⟨m⟩}φ|² ≥ 0) Therefore: dm² = inf Am ≥ inf ∫₀¹ ∫ Γ(φ,φ) dρ_t dt = W₂²
The Wasserstein distance from the squared distance
Equations
- Frourio.W2_BB Γ ρ₀ ρ₁ = √(Frourio.W2_squared_BB Γ ρ₀ ρ₁)
Instances For
Enhanced domination at the distance level: dm ≥ W₂
Flag-free domination: removing dependence on DynDistanceFlags. This completes the goal of section 1-4.
The probability space P₂(X) with finite second moments
- val : MeasureTheory.Measure X
The underlying measure
- is_prob : MeasureTheory.IsProbabilityMeasure self.val
It's a probability measure
Has finite second moment
Instances For
TopologicalSpace instance for P2. We use a discrete topology for now.
Equations
dm defines a metric on P₂(X)
Equations
- One or more equations did not get rendered due to their size.
SpectralPenalty provides an upper bound for the multi-scale term
Lower semicontinuity bridge: Am LSC implies dm_squared LSC
Zero distance identity: dm_squared(ρ, ρ) = 0 The diagonal distance vanishes because the constant curve ρ(t) = ρ for all t with zero velocity potential φ(t,x) = 0 achieves zero action.
Non-negativity: dm_squared ≥ 0 This follows from Am_nonneg since dm_squared is the infimum of non-negative values.
Symmetry: dm_squared(ρ₀, ρ₁) = dm_squared(ρ₁, ρ₀) This follows from time-reversal symmetry of the action functional.
Triangle inequality for dm_squared: subadditivity via curve gluing dm_squared(ρ₀, ρ₂) ≤ dm_squared(ρ₀, ρ₁) + dm_squared(ρ₁, ρ₂)
Triangle inequality for dm: the actual distance function dm(ρ₀, ρ₂) ≤ dm(ρ₀, ρ₁) + dm(ρ₁, ρ₂)
Flag-free pseudometric instance
Equations
- One or more equations did not get rendered due to their size.