OAI/Geometry/RCD/Harmonic/CanonicalRadialSize.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.distanceDatum_energy_bound line 17
2. theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.radialPairing_size line 43

   Source documentation

   The raw radial target of every original covector is bounded in the current normalizing frame. This supplies the vanishing affine-center bound.

   theorem DyadicDistanceReplacements.radialPairing_size
       {n : ℕ} {κ r0 B J C ε : ℝ} {p : X} {S : DyadicDistanceSources μ hQ n κ p r0}
       (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ) {r : ℝ}
       (hr : 0 ≤ r) (hrr : r ≤ 4 * distanceSourceRadius r0 i)
       (hfin : μ (ball p r) ≠ ∞) (hzero : μ (ball p r) ≠ 0) (hε : 0 ≤ ε)
       (u : Fin n → SobolevSpace μ hQ) (F : Euclidean n ≃L[ℝ] Euclidean n)
       (hgrad : ∀ j, ∀ᵐ x ∂μ.restrict (ball p r),
         localGamma μ hQ (transformedColumn μ hQ u F j) (transformedColumn μ hQ u F j) x ≤ (1 + ε) ^ 2)
       (b : Euclidean n) {H : ℝ}
       (ha : ∀ᵐ x ∂μ.restrict (ball p r),
         localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ≤ H) :
       ‖normalizeLocalL2 μ (ball p r) hfin
   …

   Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.normalizeLocalL2