AffineGlobalAssembly.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.InCutCell.abs_sub_lt line 16

Source documentation

The closed cell between neighboring cuts is contained in the corresponding open localization neighborhood, including all endpoint and tie cases.

theorem InCutCell.abs_sub_lt {n : ℕ} {q : Fin n → ℝ}
    {a b : ℝ} {t ρ : Fin (n + 1) → ℝ}
    (hfirst : t 0 - ρ 0 < a)
    (hlast : b < t (Fin.last n) + ρ (Fin.last n))
    (hcuts : ∀ i : Fin n,
      q i ∈ Set.Ioo (t i.castSucc - ρ i.castSucc) (t i.castSucc + ρ i.castSucc) ∧
      q i ∈ Set.Ioo (t i.succ - ρ i.succ) (t i.succ + ρ i.succ))
    {j : Fin (n + 1)} {μ : ℝ} (hcell : InCutCell q a b j μ) :
    |μ - t j| < ρ j := by
…

Mentions: OAI.Problem326.Affine.InCutCell

structure OAI.Problem326.Affine.LocalFamilyData line 54
Source documentation
All data needed from one fixed-minimum construction after its localization radius has been shrunk to retain a stronger offset decay exponent.
```
structure LocalFamilyData (d : ℕ) [NeZero d] (a b t : ℝ)
    (E : (Fin d → ℝ) → ℝ) where
…
```

theorem OAI.Problem326.Affine.localFamilyData_nonempty_of_fixedMinimum line 74

Source documentation

The fixed-minimum theorem and stronger individual big-O exponents supply exactly the local data required for global gluing.

theorem localFamilyData_nonempty_of_fixedMinimum {d : ℕ} [NeZero d]
    (a b t : ℝ) (E : (Fin d → ℝ) → ℝ) (Λ : Finset (Label d))
    (hbase : (⟨fun _ => t, fun _ => 0⟩ : Label d) ∈ Λ)
    (hcube : ∀ L ∈ Λ, Cube a b L.slope)
    (hlower : ∀ L ∈ Λ, ∀ k, t ≤ L.slope k)
    (hdecay : ∀ L ∈ Λ, ∃ β : ℝ, t < β ∧
      L.offset =O[𝓝[>] (0 : ℝ)] (fun h => h ^ β))
    (happrox : ApproximatesAtMinimum Λ a b t E) :
    Nonempty (LocalFamilyData d a b t E) := by
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.ApproximatesAtMinimum, OAI.Problem326.Affine.LocalFamilyData

theorem OAI.Problem326.Affine.offset_isLittleO_of_exponent_lt line 95

Source documentation

A convenient strict-power comparison for offset decay.

theorem offset_isLittleO_of_exponent_lt {c : ℝ → ℝ} {a b : ℝ}
    (hc : c =o[𝓝[>] (0 : ℝ)] (fun h => h ^ b)) (hab : a < b) :
    c =o[𝓝[>] (0 : ℝ)] (fun h => h ^ a) := by
…

theorem OAI.Problem326.Affine.exists_global_family_of_local_data line 108
Source documentation
Complete global gluing: one localized family at every possible minimum level gives a fixed finite family on the whole exponent cube. The only input not discharged here is existence of the fixed-minimum local families.
```
theorem exists_global_family_of_local_data {d : ℕ} [NeZero d]
    {a b : ℝ} (hab : a ≤ b) (E : (Fin d → ℝ) → ℝ)
    (hdata : ∀ t ∈ Set.Icc a b, Nonempty (LocalFamilyData d a b t E)) :
    ∃ Λ : Finset (Label d), Λ.Nonempty ∧
      (∀ L ∈ Λ, Cube a b L.slope ∧
        L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ a)) ∧
      ApproximatesOnCube Λ a b E := by
…
```
Mentions: OAI.Problem326.Affine.LocalFamilyData, OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.ApproximatesOnCube

theorem OAI.Problem326.Affine.exists_global_family_of_fixedMinimum line 169

Source documentation

Direct interface for the dimension induction: fixed-minimum families with individual stronger big-O exponents imply the complete affine approximation lemma in that dimension.

theorem exists_global_family_of_fixedMinimum {d : ℕ} [NeZero d]
    {a b : ℝ} (hab : a ≤ b) (E : (Fin d → ℝ) → ℝ)
    (hfixed : ∀ t ∈ Set.Icc a b, ∃ Λ : Finset (Label d),
      (⟨fun _ => t, fun _ => 0⟩ : Label d) ∈ Λ ∧
      (∀ L ∈ Λ, Cube a b L.slope) ∧
      (∀ L ∈ Λ, ∀ k, t ≤ L.slope k) ∧
      (∀ L ∈ Λ, ∃ β : ℝ, t < β ∧
        L.offset =O[𝓝[>] (0 : ℝ)] (fun h => h ^ β)) ∧
      ApproximatesAtMinimum Λ a b t E) :
    ∃ Λ : Finset (Label d), Λ.Nonempty ∧
      (∀ L ∈ Λ, Cube a b L.slope ∧
        L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ a)) ∧
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.ApproximatesAtMinimum