RegularPatchMassEnvelope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RegularPointCoordinates.rawPinchingMass line 17
Source documentation
The raw full mass before conjugation by the patch's mean.
```
def rawPinchingMass (M : PositiveBilinearMeasure X E) (n : ℕ)
    (R : ℝ) (z : X) (i : ℕ) : E →L[ℝ] E :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
def OAI.RegularPointCoordinates.patchEnvelopeFactor line 23
Source documentation
The scaling ratio from the source radius to the enclosing dyadic mass.
```
def patchEnvelopeFactor (n : ℕ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.rawPinchingMass_le_envelope line 28
Source documentation
A patch lying within one twelfth of the mean radius is contained in the preceding central dyadic mass ball, a term of the actual heat envelope.
```
theorem rawPinchingMass_le_envelope (M : PositiveBilinearMeasure X E) (n : ℕ)
    {R : ℝ} (hR : 0 < R) {q z : X} (i : ℕ)
    (hroom : dist z q ≤ (R / (2 : ℝ) ^ (i + 15)) / 12) (v : E) :
    ⟪v, rawPinchingMass M n R z i v⟫_ℝ ≤
      patchEnvelopeFactor n * ⟪v, dyadicBochnerEnvelope M n q R (i + 17) v⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.rawPinchingMass, OAI.RegularPointCoordinates.patchEnvelopeFactor, OAI.RegularPointCoordinates.dyadicBochnerEnvelope