AffineFitDifference.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Consecutive actual affine fits and their center values

theorem OAI.RegularPointCoordinates.normalized_affineFit_difference line 17

Source documentation

On a nested pair of fitting sets, the difference of the actual fits is controlled by the two residuals, with the exact normalized volume loss.

theorem normalized_affineFit_difference (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (s t : Set X) (hts : t ⊆ s)
    (hs : μ s ≠ ∞) (ht : μ t ≠ ∞) (hs0 : μ s ≠ 0) (ht0 : μ t ≠ 0)
    (f : Lp ℝ 2 (μ.restrict s)) (c d : ℝ) (a b : Euclidean n)
    (hc : affineProjection μ hQ u s hs f = affineCoordinateMap μ hQ u s hs (c, a))
    (hd : affineProjection μ hQ u t ht (localL2Restriction μ s t hts f) =
      affineCoordinateMap μ hQ u t ht (d, b)) :
    ‖normalizeLocalL2 μ t ht (affineCoordinateMap μ hQ u t ht (c - d, a - b))‖ ≤
      (Real.sqrt (μ.real s) / Real.sqrt (μ.real t)) *
        ‖normalizeLocalL2 μ s hs (affineResidual μ hQ u s hs f)‖ +
      ‖normalizeLocalL2 μ t ht
        (affineResidual μ hQ u t ht (localL2Restriction μ s t hts f))‖ := by
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineProjection, OAI.RegularPointCoordinates.affineCoordinateMap, OAI.RegularPointCoordinates.localL2Restriction, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.affineResidual

theorem OAI.RegularPointCoordinates.affineFit_center_difference line 49

Source documentation

Mean-value evaluation removes the constant term quantitatively from consecutive least-squares fits. The coefficients need not be unique.

theorem affineFit_center_difference {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n) {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (r R : ℝ) (_hr : 0 < r) (hrR : r ≤ R), -κ ≤ K * r ^ 2 →
    ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (v : X → Euclidean n),
      (∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) (u i)) →
      ContinuousOn v (ball p r) →
      (∀ i, SobolevSpace.toLp (hausdorff n X) hX.quadratic (u i) =ᵐ[
        (hausdorff n X).restrict (ball p r)] fun x => v x i) →
    ∀ η : SobolevSpace (hausdorff n X) hX.quadratic,
      (SobolevSpace.toLp (hausdorff n X) hX.quadratic η =ᵐ[
        (hausdorff n X).restrict (ball p r)] fun _ => (1 : ℝ)) →
    let μ := hausdorff n X
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp