LocalProjectionMeasure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Measured projection coordinates from local harmonic representatives

theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.measurable_values line 17

Source documentation

A measurable extension retains the same local harmonic representative.

theorem FirstOrderSplittingOn.measurable_values {μ : Measure X}
    {hQ : QuadraticCheegerEnergy μ} {n : ℕ} {q : X} {r epsilon : ℝ}
    {u : Fin n → SobolevSpace μ hQ} {V : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ q r epsilon u V) :
    ∃ W : X → Euclidean n, Measurable W ∧ EqOn V W (ball q r) ∧
      FirstOrderSplittingOn μ hQ q r epsilon u W := by
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn

theorem OAI.RegularPointCoordinates.projection_measured_local_coordinates line 33

Source documentation

The local harmonic coordinates admit a measurable representative with exactly the same metric data and the required measured approximation.

theorem projection_measured_local_coordinates {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (hmeasured : LocalMeasuredCoordinateInput hX) {error : ℝ} (herror : 0 < error) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ {q : X} {s epsilon : ℝ}, 0 < s →
      -delta / 32 ≤ K * s ^ 2 →
      ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
        (V : X → Euclidean n),
      FirstOrderSplittingOn (hausdorff n X) hX.quadratic q (2 * s) epsilon u V →
      V q = 0 →
      IsPointedApproximation q 0 (s / 64) 4 delta (fun x => (s / 64)⁻¹ • V x) →
      ∃ W : X → Euclidean n, Measurable W ∧ EqOn V W (ball q (2 * s)) ∧
        FirstOrderSplittingOn (hausdorff n X) hX.quadratic q (2 * s) epsilon u W ∧
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.IsPointedApproximation