PatchCenters.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed centers for directional patch energies

This is the selection in equation re:fixed-center: a positive lower energy floor permits one fixed point in each patch with energy at most twice every active point's energy. No continuity or measurability of the energy function is used. Directional pair bounds then give the actual fixed-center bound used to construct the correction fields.

theorem OAI.RegularPointCoordinates.exists_energy_center line 20
theorem OAI.RegularPointCoordinates.exists_patch_energy_centers line 40

theorem OAI.RegularPointCoordinates.centered_patch_energy_le line 56

Source documentation

The pairwise directional estimate becomes a bound against the energy at the testing point alone after the fixed-center selection.

theorem centered_patch_energy_le (u : X → E) (D : E →L[ℝ] E)
    {energy : X → ℝ} {C r : ℝ} {x z : X} (hC : 0 ≤ C)
    (hz : energy z ≤ 2 * energy x)
    (hpair : ⟪u x - u z, D (u x - u z)⟫_ℝ ≤
      C * r ^ 2 * (energy x + energy z)) :
    ⟪u x - u z, D (u x - u z)⟫_ℝ ≤ (3 * C) * r ^ 2 * energy x := by
…

theorem OAI.RegularPointCoordinates.exists_patch_centers_with_energy_bound line 71

Source documentation

Simultaneous construction of the fixed affine centers for a family of patches. The conclusion is the displacement-energy hypothesis used by PatchIterationGeometry, without adding regularity to the energies.

theorem exists_patch_centers_with_energy_bound
    (patch : ι → Set X) (energy : X → ℝ) (u : X → E)
    (D : ι → E →L[ℝ] E) {C r : ℝ} (hC : 0 ≤ C)
    (hne : ∀ j, (patch j).Nonempty)
    (hfloor : ∀ j, ∃ floor : ℝ, 0 < floor ∧ ∀ x ∈ patch j, floor ≤ energy x)
    (hpair : ∀ j, ∀ x ∈ patch j, ∀ z ∈ patch j,
      ⟪u x - u z, D j (u x - u z)⟫_ℝ ≤ C * r ^ 2 * (energy x + energy z)) :
    ∃ center : ι → X, ∀ j, center j ∈ patch j ∧ ∀ x ∈ patch j,
      ⟪u x - u (center j), D j (u x - u (center j))⟫_ℝ ≤
        (3 * C) * r ^ 2 * energy x := by
…