PatchJetBounds.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Higher jets of finite cutoff-affine patch fields

Only two terms survive in a higher product derivative: all derivatives on the cutoff, or one on the affine factor. Iterated Fréchet derivative bounds follow from the cutoff jets.

theorem OAI.RegularPointCoordinates.fderiv_affine_patch line 29
Source documentation
The derivative of an affine patch is the fixed patch operator.
```
theorem fderiv_affine_patch (D : E →L[ℝ] F) (c : E) :
    fderiv ℝ (fun y => D (y - c)) = fun _ => D := by
…
```

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_affine_patch line 35

Source documentation

All derivatives of an affine patch above order one vanish.

theorem norm_iteratedFDeriv_affine_patch (D : E →L[ℝ] F) (c x : E) (m : ℕ) :
    ‖iteratedFDeriv ℝ m (fun y => D (y - c)) x‖ =
      if m = 0 then ‖D (x - c)‖ else if m = 1 then ‖D‖ else 0 := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_smul_le_at line 47

Source documentation

Point-local version of the higher scalar-product bound.

theorem norm_iteratedFDeriv_smul_le_at
    {f : E → ℝ} {g : E → F} {x : E} {m : ℕ}
    (hf : ContDiffAt ℝ m f x) (hg : ContDiffAt ℝ m g x) :
    ‖iteratedFDeriv ℝ m (fun y => f y • g y) x‖ ≤
      ∑ i ∈ Finset.range (m + 1), (m.choose i : ℝ) *
        ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (m - i) g x‖ := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_cutoff_affine_le line 68

Source documentation

The two surviving terms in a higher cutoff-affine derivative.

theorem norm_iteratedFDeriv_cutoff_affine_le
    (D : E →L[ℝ] F) (c x : E) {phi : E → ℝ} {m : ℕ}
    (hphi : ContDiffAt ℝ (m + 1) phi x) :
    ‖iteratedFDeriv ℝ (m + 1) (fun y => phi y • D (y - c)) x‖ ≤
      ‖iteratedFDeriv ℝ (m + 1) phi x‖ * ‖D (x - c)‖ +
      (m + 1 : ℝ) * ‖iteratedFDeriv ℝ m phi x‖ * ‖D‖ := by
…

theorem OAI.RegularPointCoordinates.iteratedFDeriv_cutoff_affine_eq_zero_of_not_mem_tsupport line 96
Source documentation
Multiplication by a cutoff cannot create derivative support outside the cutoff support, including at its boundary.
```
theorem iteratedFDeriv_cutoff_affine_eq_zero_of_not_mem_tsupport
    (D : E →L[ℝ] F) (c x : E) (phi : E → ℝ) (m : ℕ)
    (hx : x ∉ tsupport phi) :
    iteratedFDeriv ℝ m (fun y => phi y • D (y - c)) x = 0 := by
…
```
theorem OAI.RegularPointCoordinates.cutoff_affine_gevrey_weight_le line 107
Source documentation
The derivative falling on the affine factor fits in the same Gevrey-two weight as the term falling wholly on the cutoff.
```
theorem cutoff_affine_gevrey_weight_le {C : ℝ} (hC : 1 ≤ C) (m : ℕ) :
    (m + 1 : ℝ) * C ^ (m + 1) * (m.factorial : ℝ) ^ 2 ≤
      C ^ (m + 2) * ((m + 1).factorial : ℝ) ^ 2 := by
…
```

theorem OAI.RegularPointCoordinates.scaled_cutoff_affine_jet_le line 127

Source documentation

A cutoff-affine term obeys a uniform Gevrey-two estimate at every order, including its value. The small operator and displacement bounds are premises; the conclusion is derived from the actual product rule.

theorem scaled_cutoff_affine_jet_le
    (D : E →L[ℝ] F) (c x : E) {phi : E → ℝ} {m : ℕ}
    {epsilon r L C : ℝ} (hepsilon : 0 ≤ epsilon) (hr : 0 < r)
    (_hL : 0 ≤ L) (hC : 1 ≤ C) (hD : ‖D‖ ≤ epsilon)
    (hvalue : ‖D (x - c)‖ ≤ epsilon * L * r)
    (hphi : ContDiffAt ℝ m phi x)
    (hcutoff : ∀ q ≤ m, r ^ q * ‖iteratedFDeriv ℝ q phi x‖ ≤
      C ^ (q + 1) * (q.factorial : ℝ) ^ 2) :
    r ^ m * ‖iteratedFDeriv ℝ m (fun y => phi y • D (y - c)) x‖ ≤
      epsilon * r * (L + 1) * C ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

theorem OAI.RegularPointCoordinates.iteratedFDeriv_patchField line 190

Source documentation

The finite patch field has the sum of its actual patch derivatives.

theorem iteratedFDeriv_patchField (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) (m : ℕ)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x) :
    iteratedFDeriv ℝ m (patchField s phi D c) x =
      ∑ j ∈ s, iteratedFDeriv ℝ m (fun y => phi j y • D j (y - c j)) x := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_patchField_le line 201

Source documentation

In a positive derivative order, only two cutoff orders are needed.

theorem norm_iteratedFDeriv_patchField_le (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) (m : ℕ)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ (m + 1) (phi j) x) :
    ‖iteratedFDeriv ℝ (m + 1) (patchField s phi D c) x‖ ≤
      ∑ j ∈ s, (‖iteratedFDeriv ℝ (m + 1) (phi j) x‖ * ‖D j (x - c j)‖ +
        (m + 1 : ℝ) * ‖iteratedFDeriv ℝ m (phi j) x‖ * ‖D j‖) := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.iteratedFDeriv_patchField_eq_active line 212

Source documentation

Every higher field jet can be restricted to the active cutoffs.

theorem iteratedFDeriv_patchField_eq_active (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) (m : ℕ)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x) :
    iteratedFDeriv ℝ m (patchField s phi D c) x =
      iteratedFDeriv ℝ m (patchField (s.filter (fun j => x ∈ tsupport (phi j))) phi D c) x := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.scaled_patchField_jet_le line 230

Source documentation

Summing the actual patch jets costs only the number of active terms.

theorem scaled_patchField_jet_le (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) (m : ℕ)
    {epsilon r L C : ℝ} (hepsilon : 0 ≤ epsilon) (hr : 0 < r)
    (hL : 0 ≤ L) (hC : 1 ≤ C)
    (hD : ∀ j ∈ s, ‖D j‖ ≤ epsilon)
    (hvalue : ∀ j ∈ s, ‖D j (x - c j)‖ ≤ epsilon * L * r)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x)
    (hcutoff : ∀ j ∈ s, ∀ q ≤ m,
      r ^ q * ‖iteratedFDeriv ℝ q (phi j) x‖ ≤ C ^ (q + 1) * (q.factorial : ℝ) ^ 2) :
    r ^ m * ‖iteratedFDeriv ℝ m (patchField s phi D c) x‖ ≤
      epsilon * r * (s.card : ℝ) * (L + 1) * C ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.patchField

def OAI.RegularPointCoordinates.patchJetBase line 253
Source documentation
A fixed base absorbs the overlap and center-displacement constants.
```
def patchJetBase (N L C : ℝ) : ℝ := C * max 1 (N * (L + 1))
```
theorem OAI.RegularPointCoordinates.patchJetBase_ge_one line 255

theorem OAI.RegularPointCoordinates.patchField_scaled_gevrey_two line 263

Source documentation

Uniform all-order Gevrey-two field estimate, with base independent of the derivative order and the size of the ambient net.

theorem patchField_scaled_gevrey_two (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) (m : ℕ)
    {epsilon r L C N : ℝ} (hepsilon : 0 ≤ epsilon) (hr : 0 < r)
    (hL : 0 ≤ L) (hC : 1 ≤ C) (hcard : (s.card : ℝ) ≤ N)
    (hD : ∀ j ∈ s, ‖D j‖ ≤ epsilon)
    (hvalue : ∀ j ∈ s, ‖D j (x - c j)‖ ≤ epsilon * L * r)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x)
    (hcutoff : ∀ j ∈ s, ∀ q ≤ m,
      r ^ q * ‖iteratedFDeriv ℝ q (phi j) x‖ ≤ C ^ (q + 1) * (q.factorial : ℝ) ^ 2) :
    r ^ m * ‖iteratedFDeriv ℝ m (patchField s phi D c) x‖ ≤
      epsilon * r * (patchJetBase N L C) ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.patchField, OAI.RegularPointCoordinates.patchJetBase

theorem OAI.RegularPointCoordinates.patchField_scaled_gevrey_two_active line 293

Source documentation

The uniform estimate for the full field counts only cutoffs whose closed supports contain the testing point.

theorem patchField_scaled_gevrey_two_active (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) (m : ℕ)
    {epsilon r L C N : ℝ} (hepsilon : 0 ≤ epsilon) (hr : 0 < r)
    (hL : 0 ≤ L) (hC : 1 ≤ C)
    (hcard : ((s.filter (fun j => x ∈ tsupport (phi j))).card : ℝ) ≤ N)
    (hD : ∀ j ∈ s, x ∈ tsupport (phi j) → ‖D j‖ ≤ epsilon)
    (hvalue : ∀ j ∈ s, x ∈ tsupport (phi j) → ‖D j (x - c j)‖ ≤ epsilon * L * r)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x)
    (hcutoff : ∀ j ∈ s, x ∈ tsupport (phi j) → ∀ q ≤ m,
      r ^ q * ‖iteratedFDeriv ℝ q (phi j) x‖ ≤ C ^ (q + 1) * (q.factorial : ℝ) ^ 2) :
    r ^ m * ‖iteratedFDeriv ℝ m (patchField s phi D c) x‖ ≤
      epsilon * r * (patchJetBase N L C) ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.patchField, OAI.RegularPointCoordinates.patchJetBase

theorem OAI.RegularPointCoordinates.patchField_scaled_directional_gevrey_two_active line 315

Source documentation

Every repeated directional derivative obeys the same uniform field bound, with the expected power of the direction norm.

theorem patchField_scaled_directional_gevrey_two_active
    (s : Finset ι) (phi : ι → E → ℝ) (D : ι → E →L[ℝ] E)
    (c : ι → E) (x xi : E) (m : ℕ)
    {epsilon r L C N : ℝ} (hepsilon : 0 ≤ epsilon) (hr : 0 < r)
    (hL : 0 ≤ L) (hC : 1 ≤ C)
    (hcard : ((s.filter (fun j => x ∈ tsupport (phi j))).card : ℝ) ≤ N)
    (hD : ∀ j ∈ s, x ∈ tsupport (phi j) → ‖D j‖ ≤ epsilon)
    (hvalue : ∀ j ∈ s, x ∈ tsupport (phi j) → ‖D j (x - c j)‖ ≤ epsilon * L * r)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x)
    (hcutoff : ∀ j ∈ s, x ∈ tsupport (phi j) → ∀ q ≤ m,
      r ^ q * ‖iteratedFDeriv ℝ q (phi j) x‖ ≤ C ^ (q + 1) * (q.factorial : ℝ) ^ 2) :
    r ^ m * ‖iteratedFDeriv ℝ m (patchField s phi D c) x (fun _ => xi)‖ ≤
…

Mentions: OAI.RegularPointCoordinates.patchField