RadialPairingSize.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The averaged size of the actual radial pairing

theorem OAI.RegularPointCoordinates.normalized_gamma_size line 19

Source documentation

Pointwise gradient bounds give the normalized L² size used to show that the center values of affine fits vanish at shrinking radii.

theorem normalized_gamma_size (s : Set X) (hs : μ s ≠ ∞) (hs0 : μ s ≠ 0)
    (q a : SobolevSpace μ hQ) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hq : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ q q x ≤ A)
    (ha : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ a a x ≤ B) :
    ‖normalizeLocalL2 μ s hs
      ((localGamma_memLp_two_of_bound μ hQ s q a ha).toLp (localGamma μ hQ q a))‖ ≤
        Real.sqrt (A * B) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.localGamma_memLp_two_of_bound