FieldEstimates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

First derivatives of the value-space patch field

The local mass operators may be singular. Their positivity controls the error from differentiating the cutoffs by the directional mass, rather than by the full norm of the local metric.

def OAI.RegularPointCoordinates.patchField line 21
Source documentation
The field used by the renormalization, written as a finite patch sum.
```
def patchField (s : Finset ι) (phi : ι → E → ℝ) (D : ι → E →L[ℝ] E)
    (c : ι → E) (P : E) : E :=
…
```

theorem OAI.RegularPointCoordinates.hasFDerivAt_patchField line 26

Source documentation

Its derivative consists of the principal positive mass plus cutoff errors.

theorem hasFDerivAt_patchField (s : Finset ι) (phi : ι → E → ℝ)
    (dphi : ι → E →L[ℝ] ℝ) (D : ι → E →L[ℝ] E) (c : ι → E) (P : E)
    (hphi : ∀ j ∈ s, HasFDerivAt (phi j) (dphi j) P) :
    HasFDerivAt (patchField s phi D c)
      (∑ j ∈ s, ((phi j P) • D j + (dphi j).smulRight (D j (P - c j)))) P := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.patch_error_inner_le line 42

Source documentation

A finite cutoff error is bounded by the square root of the directional mass times the square root of the displacement energy.

theorem patch_error_inner_le (s : Finset ι) (D : ι → E →L[ℝ] E)
    (w : ι → E) (a : ι → ℝ) (xi : E) {K : ℝ} (hK : 0 ≤ K)
    (hD : ∀ j ∈ s, (D j).IsPositive) (ha : ∀ j ∈ s, |a j| ≤ K) :
    |⟪xi, ∑ j ∈ s, a j • D j (w j)⟫_ℝ| ≤
      K * Real.sqrt (∑ j ∈ s, ⟪xi, D j xi⟫_ℝ) *
        Real.sqrt (∑ j ∈ s, ⟪w j, D j (w j)⟫_ℝ) := by
…

theorem OAI.RegularPointCoordinates.patch_principal_isPositive line 76

Source documentation

The principal part of the derivative is positive when the cutoffs are.

theorem patch_principal_isPositive (s : Finset ι) (phi : ι → ℝ)
    (D : ι → E →L[ℝ] E)
    (hphi : ∀ j ∈ s, 0 ≤ phi j) (hD : ∀ j ∈ s, (D j).IsPositive) :
    (∑ j ∈ s, phi j • D j).IsPositive := by
…