OAI/Geometry/WeakHessian/Model.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakHessian.Time line 12

   Also declared: ComparatorChallenges/WeakHessian.lean:12 (same declaration text).

2. def OAI.WeakHessian.timeZero line 14

   Also declared: ComparatorChallenges/WeakHessian.lean:14 (same declaration text).

3. def OAI.WeakHessian.timeOne line 15

   Also declared: ComparatorChallenges/WeakHessian.lean:15 (same declaration text).

4. def OAI.WeakHessian.clampTime line 17

   Also declared: ComparatorChallenges/WeakHessian.lean:17 (same declaration text).

5. abbrev OAI.WeakHessian.Curve line 22

   Also declared: ComparatorChallenges/WeakHessian.lean:22 (same declaration text).

6. instance OAI.WeakHessian.curveMeasurableSpace line 24

   Also declared: ComparatorChallenges/WeakHessian.lean:24 (same declaration text).

7. instance OAI.WeakHessian.curveBorelSpace line 26

   Also declared: ComparatorChallenges/WeakHessian.lean:26 (same declaration text).

8. def OAI.WeakHessian.evalReal line 28

   Also declared: ComparatorChallenges/WeakHessian.lean:28 (same declaration text).

9. def OAI.WeakHessian.IsGeodesic line 31

   Source documentation

   The constant-speed minimizing parametrization, including constant curves.

   Also declared: ComparatorChallenges/WeakHessian.lean:31 (same declaration text).

   def IsGeodesic (γ : Curve X) : Prop :=
   …

   Mentions: OAI.WeakHessian.Curve

10. def OAI.WeakHessian.metricSpeed line 36

    Source documentation

    Metric speed. Limsup agrees a.e. with the metric derivative on AC² curves.

    Also declared: ComparatorChallenges/WeakHessian.lean:36 (same declaration text).

    def metricSpeed (γ : Curve X) (t : ℝ) : ℝ≥0∞ :=
    …

    Mentions: OAI.WeakHessian.Curve

11. def OAI.WeakHessian.IsAC2 line 41

    Source documentation

    Absolute continuity with a square-integrable metric control.

    Also declared: ComparatorChallenges/WeakHessian.lean:41 (same declaration text).

    def IsAC2 (γ : Curve X) : Prop :=
    …

    Mentions: OAI.WeakHessian.Curve

12. def OAI.WeakHessian.IsTestPlan line 50

    Source documentation

    A 2-test plan: bounded compression and finite average kinetic energy.

    Also declared: ComparatorChallenges/WeakHessian.lean:50 (same declaration text).

    def IsTestPlan (m : Measure X) (π : Measure (Curve X)) : Prop :=
    …

    Mentions: OAI.WeakHessian.Curve

13. def OAI.WeakHessian.BoundedTracks line 58

    Source documentation

    Uniform bounded spatial support; used only to define the local Sobolev class.

    Also declared: ComparatorChallenges/WeakHessian.lean:58 (same declaration text).

    def BoundedTracks (π : Measure (Curve X)) : Prop :=
    …

    Mentions: OAI.WeakHessian.Curve

14. def OAI.WeakHessian.LocallyL2 line 61

    Also declared: ComparatorChallenges/WeakHessian.lean:61 (same declaration text).

15. def OAI.WeakHessian.IsLocalWeakUpperGradient line 65

    Source documentation

    Local weak upper gradients, in the integrated test-plan definition.

    Also declared: ComparatorChallenges/WeakHessian.lean:65 (same declaration text).

    def IsLocalWeakUpperGradient (m : Measure X) (f D : X → ℝ) : Prop :=
    …

16. def OAI.WeakHessian.IsMinimalLocalWeakUpperGradient line 72

    Also declared: ComparatorChallenges/WeakHessian.lean:72 (same declaration text).

17. def OAI.WeakHessian.weakGradient line 77

    Source documentation

    A representative of the minimal weak upper gradient (zero off its domain).

    Also declared: ComparatorChallenges/WeakHessian.lean:77 (same declaration text).

    def weakGradient (m : Measure X) (f : X → ℝ) : X → ℝ :=
    …

18. def OAI.WeakHessian.LocalSobolev line 81

    Also declared: ComparatorChallenges/WeakHessian.lean:81 (same declaration text).

19. def OAI.WeakHessian.Sobolev line 84

    Also declared: ComparatorChallenges/WeakHessian.lean:84 (same declaration text).

20. def OAI.WeakHessian.gamma line 88

    Source documentation

    Polarization of the minimal weak gradient on an infinitesimally Hilbertian space.

    Also declared: ComparatorChallenges/WeakHessian.lean:88 (same declaration text).

    def gamma (m : Measure X) (f g : X → ℝ) (x : X) : ℝ :=
    …

21. def OAI.WeakHessian.IsLaplacian line 93

    Source documentation

    Weak nonpositive generator convention, without a global L² assumption on F.

    Also declared: ComparatorChallenges/WeakHessian.lean:93 (same declaration text).

    def IsLaplacian (m : Measure X) (u L : X → ℝ) : Prop :=
    …

22. def OAI.WeakHessian.InLaplacianDomain line 98

    Also declared: ComparatorChallenges/WeakHessian.lean:98 (same declaration text).

23. def OAI.WeakHessian.laplacian line 101

    Also declared: ComparatorChallenges/WeakHessian.lean:101 (same declaration text).

24. def OAI.WeakHessian.BoundedFunction line 104

    Also declared: ComparatorChallenges/WeakHessian.lean:104 (same declaration text).

25. def OAI.WeakHessian.GloballyLipschitz line 106

    Also declared: ComparatorChallenges/WeakHessian.lean:106 (same declaration text).

26. def OAI.WeakHessian.IsTestFunction line 109

    Source documentation

    Bounded globally Lipschitz Laplacian-domain functions with Sobolev Laplacian.

    Also declared: ComparatorChallenges/WeakHessian.lean:109 (same declaration text).

    def IsTestFunction (m : Measure X) (g : X → ℝ) : Prop :=
    …

27. def OAI.WeakHessian.weakHessian line 114

    Source documentation

    The weak Hessian, with ∇_(∇g)∇g = ∇(Γ(g)/2).

    Also declared: ComparatorChallenges/WeakHessian.lean:114 (same declaration text).

    def weakHessian (m : Measure X) (F g h : X → ℝ) : ℝ :=
    …

28. def OAI.WeakHessian.WeakHessianUpperBound line 118

    Also declared: ComparatorChallenges/WeakHessian.lean:118 (same declaration text).

29. def OAI.WeakHessian.localSlope line 125

    Source documentation

    Asymptotic Lipschitz slope; zero at an isolated point.

    Also declared: ComparatorChallenges/WeakHessian.lean:125 (same declaration text).

    def localSlope (f : X → ℝ) (x : X) : ℝ≥0∞ :=
    …

30. def OAI.WeakHessian.cheegerEnergy line 129

    Source documentation

    Cheeger energy is the L² relaxation of one half the squared local slope.

    Also declared: ComparatorChallenges/WeakHessian.lean:129 (same declaration text).

    def cheegerEnergy (m : Measure X) (f : X → ℝ) : ℝ≥0∞ :=
    …

31. def OAI.WeakHessian.QuadraticCheegerEnergy line 138

    Also declared: ComparatorChallenges/WeakHessian.lean:138 (same declaration text).

32. def OAI.WeakHessian.sigmaCoeff line 144

    Source documentation

    The unreduced Lott–Sturm–Villani distortion coefficient σ.

    Also declared: ComparatorChallenges/WeakHessian.lean:144 (same declaration text).

    def sigmaCoeff (K N t θ : ℝ) : ℝ≥0∞ :=
    …

33. def OAI.WeakHessian.tauCoeff line 157

    Source documentation

    The τ coefficient (not the reduced σ coefficient) in CD(K,N).

    Also declared: ComparatorChallenges/WeakHessian.lean:157 (same declaration text).

    def tauCoeff (K N t θ : ℝ) : ℝ≥0∞ :=
    …

34. def OAI.WeakHessian.HasSecondMoment line 160

    Also declared: ComparatorChallenges/WeakHessian.lean:160 (same declaration text).

35. def OAI.WeakHessian.IsCoupling line 163

    Also declared: ComparatorChallenges/WeakHessian.lean:163 (same declaration text).

36. def OAI.WeakHessian.QuadraticTransportCost line 166

    Also declared: ComparatorChallenges/WeakHessian.lean:166 (same declaration text).

37. def OAI.WeakHessian.IsOptimalCoupling line 169

    Also declared: ComparatorChallenges/WeakHessian.lean:169 (same declaration text).

38. def OAI.WeakHessian.endpointCoupling line 173

    Also declared: ComparatorChallenges/WeakHessian.lean:173 (same declaration text).

39. def OAI.WeakHessian.interpolation line 176

    Also declared: ComparatorChallenges/WeakHessian.lean:176 (same declaration text).

40. def OAI.WeakHessian.renyiIntegral line 180

    Source documentation

    The positive of minus the N-Rényi entropy; singular mass contributes zero.

    Also declared: ComparatorChallenges/WeakHessian.lean:180 (same declaration text).

    def renyiIntegral (m μ : Measure X) (N : ℝ) : ℝ≥0∞ :=
    …

41. def OAI.WeakHessian.CurvatureDimension line 184

    Source documentation

    Unreduced CD(K,N), written with the standard dynamical optimal-plan formula.

    Also declared: ComparatorChallenges/WeakHessian.lean:184 (same declaration text).

    def CurvatureDimension (m : Measure X) (K N : ℝ) : Prop :=
    …

42. def OAI.WeakHessian.RCD line 200

    Also declared: ComparatorChallenges/WeakHessian.lean:200 (same declaration text).

43. def OAI.WeakHessian.FullSupport line 203

    Also declared: ComparatorChallenges/WeakHessian.lean:203 (same declaration text).

44. def OAI.WeakHessian.FiniteOnBoundedSets line 206

    Also declared: ComparatorChallenges/WeakHessian.lean:206 (same declaration text).

45. def OAI.WeakHessian.CurveSecondDerivativeBound line 210

    Source documentation

    The literal second-distributional-derivative conclusion on (0,1).

    Also declared: ComparatorChallenges/WeakHessian.lean:210 (same declaration text).

    def CurveSecondDerivativeBound (F G : X → ℝ) (σ : Curve X) : Prop :=
    …

    Mentions: OAI.WeakHessian.Curve