OAI/Geometry/RCD/Harmonic/DyadicRadialTargets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compatible local L2 targets for consecutive actual affine fits

  1. def OAI.RegularPointCoordinates.dyadicRadialTarget line 22
  2. theorem OAI.RegularPointCoordinates.dyadicRadialTarget_residual_norm line 29
  3. theorem OAI.RegularPointCoordinates.dyadicRadialTarget_restrict line 40

    Source documentation

    Although the compact distance primitives change with scale, their actual radial derivatives agree under restriction.

    theorem dyadicRadialTarget_restrict {i j : ℕ} (hij : i ≤ j) (b : Euclidean n) :
    let hsub := ball_subset_ball (div_le_div_of_nonneg_right
…

    Mentions: OAI.RegularPointCoordinates.Euclidean