PlanGradientMean.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Mean endpoint control from a bounded relaxed gradient

theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_mean_increment_le line 19

Source documentation

A bounded-compression geodesic plan reads the actual relaxed gradient as an upper gradient, without a compression factor in the final bound.

theorem IsRelaxedSlope.testPlan_mean_increment_le
    (π : Measure C(Time,X)) [IsProbabilityMeasure π]
    (hgeo : ∀ᵐ γ ∂π, IsGeodesic γ) {C : ℝ≥0∞} (hC : C ≠ ∞)
    (hcomp : ∀ t : Time, π.map (fun γ => γ t) ≤ C • μ)
    (hD : MemLp (fun γ : C(Time,X) => dist (γ 0) (γ 1)) 2 π)
    {D L : ℝ} (hL : 0 ≤ L) (hDb : ∀ᵐ γ ∂π, dist (γ 0) (γ 1) ≤ D)
    {u G : Lp ℝ 2 μ} (hG : IsRelaxedSlope μ u G) (hGb : ∀ᵐ x ∂μ, G x ≤ L) :
    (∫ γ : C(Time,X), |u (γ 1)-u (γ 0)| ∂π) ≤ D*L := by
…

Mentions: OAI.RegularPointCoordinates.Time, OAI.RegularPointCoordinates.IsGeodesic, OAI.RegularPointCoordinates.IsRelaxedSlope