PatchAssembly.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Patch fields as input to the analytic iteration

The frozen covector transformation sends the actual patch field to an actual cutoff-affine patch field with conjugated positive operators. The estimates here use only patch geometry and cutoff derivatives; no coordinate iterate or estimate for its derivatives is an input.

theorem OAI.RegularPointCoordinates.frozenConjugate_normalized_displacement line 28

Source documentation

Exact affine displacement under the frozen dual transformation.

theorem frozenConjugate_normalized_displacement {r : ℝ} (hr : r ≠ 0)
    (T : E ≃L[ℝ] E) (D : E →L[ℝ] E) (x c z : E) :
    frozenConjugate T D (z - r⁻¹ • T (c - x)) =
      r⁻¹ • (T.symm : E →L[ℝ] E).adjoint (D (frozenSource r T x z - c)) := by
…

Mentions: OAI.RegularPointCoordinates.frozenConjugate, OAI.RegularPointCoordinates.frozenSource

theorem OAI.RegularPointCoordinates.normalizedCovector_patchField line 41

Source documentation

Frozen normalization is an exact identity between finite patch fields.

theorem normalizedCovector_patchField {r : ℝ} (hr : r ≠ 0)
    (T : E ≃L[ℝ] E) (x : E) (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) :
    normalizedCovector r T x (patchField s phi D c) =
      patchField s (fun j z => phi j (frozenSource r T x z))
        (fun j => frozenConjugate T (D j)) (fun j => r⁻¹ • T (c j - x)) := by
…

Mentions: OAI.RegularPointCoordinates.normalizedCovector, OAI.RegularPointCoordinates.patchField, OAI.RegularPointCoordinates.frozenSource, OAI.RegularPointCoordinates.frozenConjugate

theorem OAI.RegularPointCoordinates.mem_tsupport_frozen_cutoff line 57
Source documentation
A cutoff active after normalization was active at the original center. Continuity alone gives the inclusion needed for an overlap bound.
```
theorem mem_tsupport_frozen_cutoff {r : ℝ} (T : E ≃L[ℝ] E) (x : E)
    (phi : E → ℝ) (hz : (0 : E) ∈ tsupport (fun z => phi (frozenSource r T x z))) :
    x ∈ tsupport phi := by
…
```
Mentions: OAI.RegularPointCoordinates.frozenSource

theorem OAI.RegularPointCoordinates.frozen_cutoff_active_card_le line 66

Source documentation

The number of active cutoffs does not increase under normalization.

theorem frozen_cutoff_active_card_le {r : ℝ} (T : E ≃L[ℝ] E) (x : E)
    (s : Finset ι) (phi : ι → E → ℝ) :
    (s.filter (fun j => (0 : E) ∈ tsupport (fun z => phi j (frozenSource r T x z)))).card ≤
      (s.filter (fun j => x ∈ tsupport (phi j))).card := by
…

Mentions: OAI.RegularPointCoordinates.frozenSource

theorem OAI.RegularPointCoordinates.contDiffAt_frozen_cutoff line 78
Source documentation
Cutoff smoothness at the center transports through the frozen affine map.
```
theorem contDiffAt_frozen_cutoff {r : ℝ} (T : E ≃L[ℝ] E) (x : E)
    {phi : E → ℝ} {m : ℕ} (hphi : ContDiffAt ℝ m phi x) :
    ContDiffAt ℝ m (fun z => phi (frozenSource r T x z)) 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.frozenSource

theorem OAI.RegularPointCoordinates.normalized_patch_displacement_le line 90

Source documentation

Small displacement energy gives the normalized affine value bound. The local energy budget energy ≤ epsilon is what makes this linear in epsilon, including when the positive mass operator is degenerate.

theorem normalized_patch_displacement_le {r epsilon C energy : ℝ}
    (hr : 0 < r) (hepsilon : 0 ≤ epsilon) (hC : 0 ≤ C)
    (henergy : 0 ≤ energy) (hbudget : energy ≤ epsilon)
    (T : E ≃L[ℝ] E) (D : E →L[ℝ] E) (x c : E)
    (hD : D.IsPositive) (hsmall : ∀ y, ⟪y, D y⟫_ℝ ≤ epsilon * ‖T y‖ ^ 2)
    (hvalue : ⟪x - c, D (x - c)⟫_ℝ ≤ C * r ^ 2 * energy) :
    ‖frozenConjugate T D ((0 : E) - r⁻¹ • T (c - x))‖ ≤ epsilon * Real.sqrt C := by
…

Mentions: OAI.RegularPointCoordinates.frozenConjugate

theorem OAI.RegularPointCoordinates.factorial_sq_le_majorant_scale line 111
Source documentation
The factorial target weight absorbs the Gevrey-two cutoff weight.
```
theorem factorial_sq_le_majorant_scale (m : ℕ) :
    (m.factorial : ℝ) ^ 2 ≤ factorialMajorant m * (m.factorial : ℝ) := by
…
```
Mentions: OAI.RegularPointCoordinates.factorialMajorant

theorem OAI.RegularPointCoordinates.normalized_patchField_jet_le line 125

Source documentation

Actual normalized correction jets with a fixed base, independent of order and of the full net size. Only active patches enter the estimate.

theorem normalized_patchField_jet_le
    (T : E ≃L[ℝ] E) (x : E) (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (m : ℕ)
    {r epsilon C energy L N F B : ℝ}
    (hr : 0 < r) (hepsilon : 0 ≤ epsilon) (hC : 0 ≤ C)
    (henergy : 0 ≤ energy) (hbudget : energy ≤ epsilon) (hL : 1 ≤ L)
    (hcard : ((s.filter (fun j => x ∈ tsupport (phi j))).card : ℝ) ≤ N)
    (hD : ∀ j ∈ s, x ∈ tsupport (phi j) → (D j).IsPositive)
    (hsmall : ∀ j ∈ s, x ∈ tsupport (phi j) → ∀ y,
      ⟪y, D j y⟫_ℝ ≤ epsilon * ‖T y‖ ^ 2)
    (hvalue : ∀ j ∈ s, x ∈ tsupport (phi j) →
      ⟪x - c j, D j (x - c j)⟫_ℝ ≤ C * r ^ 2 * energy)
…

theorem OAI.RegularPointCoordinates.contDiffAt_patchField line 183

Source documentation

Local smoothness of the full finite patch field.

theorem contDiffAt_patchField (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) {m : ℕ}
    (hphi : ∀ j ∈ s, ContDiffAt ℝ m (phi j) x) :
    ContDiffAt ℝ m (patchField s phi D c) x := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.patchField_eq_active_at line 194

Source documentation

At the testing point the field is the sum over active patches.

theorem patchField_eq_active_at (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x : E) :
    patchField s phi D c x =
      patchField (s.filter (fun j => x ∈ tsupport (phi j))) phi D c x := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.fderiv_patchField_eq_active_at line 207

Source documentation

The first derivative also restricts to active patches.

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

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.diagonalSecond_patchField_eq_active_at line 218

Source documentation

The actual second directional derivative restricts to active patches.

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

Mentions: OAI.RegularPointCoordinates.diagonalSecond, OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.patchField_directional_bounds line 230

Source documentation

All four directional hypotheses of the analytic iteration follow from the actual finite patches, with one common coefficient.

theorem patchField_directional_bounds
    (T : E ≃L[ℝ] E) (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (x xi : E) {N : ℕ}
    {epsilon C K r energy F : ℝ}
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1)
    (hC : 0 ≤ C) (hK : 0 ≤ K) (hr : 0 < r) (henergy : 0 ≤ energy)
    (hcard : (s.filter (fun j => x ∈ tsupport (phi j))).card ≤ N)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ 2 (phi j) x)
    (hD : ∀ j ∈ s, x ∈ tsupport (phi j) → (D j).IsPositive)
    (hphi0 : ∀ j ∈ s, x ∈ tsupport (phi j) → 0 ≤ phi j x)
    (hphi1 : ∀ j ∈ s, x ∈ tsupport (phi j) → phi j x ≤ 1)
    (hZ : ∀ y, ⟪y, patchMass (s.filter (fun j => x ∈ tsupport (phi j))) D y⟫_ℝ ≤
…

Mentions: OAI.RegularPointCoordinates.patchMass

def OAI.RegularPointCoordinates.activePatches line 333
Source documentation
Only cutoffs whose closed support contains the point are active.
```
def activePatches (s : Finset ι) (phi : ι → E → ℝ) (x : E) : Finset ι :=
…
```
structure OAI.RegularPointCoordinates.PatchIterationGeometry line 339
Source documentation
Geometric patch data before the coordinate iteration. The assumptions are on cutoffs, positive mass operators, displacement energies and their cumulative budgets; no estimate on the resulting field is assumed.
```
structure PatchIterationGeometry (Ω : Set E) (r0 Theta epsilon : ℝ)
    (N : ℕ) (C K L : ℝ) where
…
```
def OAI.RegularPointCoordinates.patchAssemblyCoefficient line 388
Source documentation
One explicit coefficient covers all directional and higher-jet bounds of the finite patch field.
```
def patchAssemblyCoefficient (N : ℕ) (C K L : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.patchAssemblyCoefficient_bounds line 393
theorem OAI.RegularPointCoordinates.PatchIterationGeometry.energy_le line 416
Source documentation
An individual nonnegative defect is bounded by the cumulative budget.
```
theorem energy_le (p : PatchIterationGeometry (ι := ι) Ω r0 Theta epsilon N C K L)
…
```
Mentions: OAI.RegularPointCoordinates.PatchIterationGeometry
def OAI.RegularPointCoordinates.PatchIterationGeometry.toAnalyticIterationData line 425
Source documentation
Assemble the analytic iteration inputs from genuine finite patch fields. The four field bounds and every correction jet are conclusions of the patch calculus, rather than fields of the geometric input.
```
def toAnalyticIterationData
    (p : PatchIterationGeometry (ι := ι) Ω r0 Theta epsilon N C K L)
…
```
Mentions: OAI.RegularPointCoordinates.PatchIterationGeometry
def OAI.RegularPointCoordinates.PatchIterationGeometry.toCanonicalAnalyticIterationData line 498
Source documentation
The explicit patch constants supply a canonical field coefficient and jet base, with no dependence on a coordinate iterate.
```
def toCanonicalAnalyticIterationData
    (p : PatchIterationGeometry (ι := ι) Ω r0 Theta epsilon N C K L)
…
```
Mentions: OAI.RegularPointCoordinates.PatchIterationGeometry

theorem OAI.RegularPointCoordinates.exists_patch_metric_iteration line 512

Source documentation

Geometric patches and cumulative budgets supply the field estimates and correction jets for the finite analytic iteration.

theorem exists_patch_metric_iteration [FiniteDimensional ℝ E]
    (N : ℕ) {Theta C K L : ℝ} (hTheta : 1 ≤ Theta)
    (hC : 0 ≤ C) (hK : 0 ≤ K) (hL : 1 ≤ L) :
    ∃ epsilon : ℝ, 0 < epsilon ∧ epsilon ≤ 1 ∧
      ∀ (Ω : Set E), IsOpen Ω → ∀ (r0 : ℝ), 0 < r0 →
      ∀ p : PatchIterationGeometry (ι := ι) Ω r0 Theta epsilon N C K L,
…

Mentions: OAI.RegularPointCoordinates.PatchIterationGeometry