NearbyExactFrames.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact frame comparison for nearby radial centers

theorem OAI.RegularPointCoordinates.nearby_exact_frames line 18

Source documentation

The quarter-error volume regime supplies the overlap ratio for two nearby same-scale exact frames. The bound has no dependence on the scale.

theorem nearby_exact_frames {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
    (p q : X) {s ε : ℝ} (hs : 0 < s) (hε : 0 ≤ ε) (hdist : dist p q ≤ s / 4)
    (Np Nq : Euclidean n ≃L[ℝ] Euclidean n) (vp vq : X → Euclidean n)
    (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (2 : ℝ) ^ n) * ε) ≤ 1 / 3)
    (hp : FirstOrderSplittingOn (hausdorff n X) hX.quadratic p (2 * s) ε (transformedColumn (hausdorff n X) hX.quadratic u Np) vp)
    (hq : FirstOrderSplittingOn (hausdorff n X) hX.quadratic q (2 * s) ε (transformedColumn (hausdorff n X) hX.quadratic u Nq) vq)
    (hep : IsExactMeanNormalization (hausdorff n X) hX.quadratic (sobolevColumnMap (hausdorff n X) hX.quadratic u) (ball p (2 * s)) measurableSet_ball Np)
    (heq : IsExactMeanNormalization (hausdorff n X) hX.quadratic (sobolevColumnMap (hausdorff n X) hX.quadratic u) (ball q (2 * s)) measurableSet_ball Nq)
    (hVp : |(hausdorff n X).real (ball p (2 * s)) / (euclideanUnitVolume n * (2 * s) ^ n) - 1| ≤ 1 / 4)
    (hVq : |(hausdorff n X).real (ball q (2 * s)) / (euclideanUnitVolume n * (2 * s) ^ n) - 1| ≤ 1 / 4)
    (hVs : |(hausdorff n X).real (ball q s) / (euclideanUnitVolume n * s ^ n) - 1| ≤ 1 / 4) :
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.euclideanUnitVolume