OAI/Geometry/RCD/Harmonic/CenteredAffineDifference.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.centeredAffineSobolev_difference_constant line 17
2. theorem OAI.RegularPointCoordinates.normalized_two_fit_difference line 46

   Source documentation

   Two approximations to the same local target control their difference. The two compact constant representatives may be different.

   theorem normalized_two_fit_difference {s : Set X} (hfin : μ s ≠ ∞)
       (t : Lp ℝ 2 (μ.restrict s)) (f g : SobolevSpace μ hQ) {A B : ℝ}
       (hf : ‖normalizeLocalL2 μ s hfin (t - SobolevSpace.restrictLp μ hQ s f)‖ ^ 2 ≤ A)
       (hg : ‖normalizeLocalL2 μ s hfin (t - SobolevSpace.restrictLp μ hQ s g)‖ ^ 2 ≤ B) :
       ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s (f - g))‖ ^ 2 ≤
         2 * A + 2 * B := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp