OAI/MeasureTheory/Falconer/Shells/DistanceLinearization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual distance Taylor error for the suffix reduction

The error estimate is dimension independent before insertion of the cube diameter. Its proof is the exact squared-norm identity, so no differentiable extension across the diagonal is needed.

  1. theorem OAI.Falconer.norm_linearization_bounds line 18
  2. theorem OAI.Falconer.norm_linearization_abs_le line 38
  3. theorem OAI.Falconer.pair_displacement_bound line 44
  4. theorem OAI.Falconer.DyadicCube.distance_linearization line 53

    Source documentation

    Original distances on a pair of small cubes have the required quadratic error relative to their center direction.

    theorem DyadicCube.distance_linearization {d : ℕ} (P Q : DyadicCube d)
    (hP : 0 < P.side) (hQ : Q.side = P.side)
    {g : ℝ} (hg : 0 < g) (hsep : g ≤ ‖P.center-Q.center‖)
    {x y : Space d} (hx : x ∈ P.carrier) (hy : y ∈ Q.carrier) :
    |dist x y-inner ℝ (‖P.center-Q.center‖⁻¹ • (P.center-Q.center)) (x-y)| ≤
      2*(d:ℝ)*P.side^2/g := by
…

    Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space