MetricDyadicNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Metric approximation in the exact dyadic normalizing frame

theorem OAI.RegularPointCoordinates.IsPointedApproximation.rescale_eight line 15
Source documentation
The half-ball output of almost splitting covers four radial testing radii after changing the physical unit by eight.
```
theorem IsPointedApproximation.rescale_eight {X : Type*} [MetricSpace X] {n : ℕ}
    {p : X} {r ε : ℝ} (hr : 0 < r) {f : X → Euclidean n}
    (hf : IsPointedApproximation p 0 (8 * r) (1 / 2) ε f) :
    IsPointedApproximation p 0 r 4 (8 * ε) (fun x => (8 : ℝ) • f x) := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.exists_metric_dyadic_normalized_family line 55

Source documentation

Choose each dyadic frame once, retaining its exact mean, splitting data and metric approximation together. The testing radius is 1/128 of the mean-normalization radius, or 1/64 of the distance-source radius.

theorem exists_metric_dyadic_normalized_family (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (v : X → Euclidean n)
    (p : X) {R T β ρ : ℝ} (hR : 0 < R) (hRT : 4 * R ≤ T)
    (hfamily : ∀ r : ℝ, 0 < r → 64 * r ≤ T →
      ∃ A : Euclidean n ≃L[ℝ] Euclidean n,
        IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
          (ball p (16 * r)) measurableSet_ball A ∧
        FirstOrderSplittingOn μ hQ p (16 * r) β (transformedColumn μ hQ u A)
          (fun x => (A : Euclidean n →L[ℝ] Euclidean n).adjoint (v x)) ∧
        IsPointedApproximation p 0 r (1 / 2) ρ (fun x => r⁻¹ •
          ((A : Euclidean n →L[ℝ] Euclidean n).adjoint (v x) -
            (A : Euclidean n →L[ℝ] Euclidean n).adjoint (v p)))) :
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsPointedApproximation