AffineGlobalGluing.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.Affine.shiftedLabel line 16
Source documentation
The cumulative shift assigned to a local family at level j.
```
def shiftedLabel {d : ℕ} (q : ℕ → ℝ) (j : ℕ) (L : Label d) : Label d :=
…
```
Mentions: OAI.Problem326.Affine.Label
def OAI.Problem326.Affine.gluedFamily line 20
Source documentation
Union of the shifted local families, with levels numbered 0, ..., N.
```
def gluedFamily {d : ℕ} (N : ℕ) (q : ℕ → ℝ)
    (Λ : ℕ → Finset (Label d)) : Finset (Label d) := by
…
```
Mentions: OAI.Problem326.Affine.Label
lemma OAI.Problem326.Affine.shiftedLabel_slope line 25
lemma OAI.Problem326.Affine.shiftedLabel_value line 28
lemma OAI.Problem326.Affine.shiftedLabel_mem_gluedFamily line 35
lemma OAI.Problem326.Affine.mem_gluedFamily_iff line 42
lemma OAI.Problem326.Affine.active_gluedFamily_restrict line 54
lemma OAI.Problem326.Affine.gluedFamily_nonempty line 63
def OAI.Problem326.Affine.Approximates line 71
Source documentation
The full sequential approximation conclusion, with unrestricted approximating exponent vectors, as required by the dimensional induction.
```
def Approximates {d : ℕ} (Λ : Finset (Label d)) (a b : ℝ)
    (E : (Fin d → ℝ) → ℝ) : Prop :=
…
```
Mentions: OAI.Problem326.Affine.Label
lemma OAI.Problem326.Affine.exists_hasMinimum line 80
Source documentation
Compactness of the coordinate index supplies a least exponent.
```
lemma exists_hasMinimum {d : ℕ} (hd : 0 < d) (p : Fin d → ℝ) :
    ∃ t, HasMinimum p t := by
…
```
Mentions: OAI.Problem326.Affine.HasMinimum

theorem OAI.Problem326.Affine.gluedFamily_approximates line 90

Source documentation

Assemble local fixed-minimum families into a global approximation family. The two decay hypotheses are precisely those ensured by choosing each cut inside both adjacent validity intervals. The local guarantees include the cut endpoints.

theorem gluedFamily_approximates {d N : ℕ} (hd : 0 < d)
    (t q : ℕ → ℝ) (Λ : ℕ → Finset (Label d)) (a b : ℝ)
    (E : (Fin d → ℝ) → ℝ)
    (hbaseline : ∀ j ≤ N, (⟨fun _ => t j, fun _ => 0⟩ : Label d) ∈ Λ j)
    (hslope : ∀ j ≤ N, ∀ L ∈ Λ j, ∀ i, t j ≤ L.slope i)
    (hcenters : ∀ j < N, t j < t (j + 1))
    (hupperdecay : ∀ j < N, ∀ L ∈ Λ j,
      L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ q j))
    (hlowerdecay : ∀ j < N, ∀ L ∈ Λ (j + 1),
      L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ q j))
    (hlocal : ∀ j ≤ N, ∀ μ ∈ Set.Icc a b,
      (j = 0 ∨ q (j - 1) ≤ μ) → (j = N ∨ μ ≤ q j) →
…

Mentions: OAI.Problem326.Affine.Label

lemma OAI.Problem326.Affine.shiftedLabel_offset_isLittleO line 172
Source documentation
Offset decay is preserved by the cumulative shifts because every cut exponent lies strictly above the lower endpoint.
```
lemma shiftedLabel_offset_isLittleO {d : ℕ} {a : ℝ} (q : ℕ → ℝ)
    (j : ℕ) (L : Label d)
    (hL : L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ a))
    (hq : ∀ k < j, a < q k) :
    (shiftedLabel q j L).offset =o[𝓝[>] 0] (fun h : ℝ => h ^ a) := by
…
```
Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.shiftedLabel

theorem OAI.Problem326.Affine.exists_approximating_family_of_local_families line 186

Source documentation

Arbitrary local radius certificates are glued into one nonempty finite family. No regularity of ρ, Γ, or E is assumed. Local guarantees on open bands suffice because all cuts lie strictly inside both neighboring bands.

theorem exists_approximating_family_of_local_families {d : ℕ} (hd : 0 < d)
    {a b : ℝ} (hab : a ≤ b) (E : (Fin d → ℝ) → ℝ)
    (ρ : ℝ → ℝ) (Γ : ℝ → Finset (Label d))
    (hρ : ∀ t ∈ Set.Icc a b, 0 < ρ t)
    (hbaseline : ∀ t ∈ Set.Icc a b,
      (⟨fun _ => t, fun _ => 0⟩ : Label d) ∈ Γ t)
    (hdata : ∀ t ∈ Set.Icc a b, ∀ L ∈ Γ t,
      Cube a b L.slope ∧ HasMinimum L.slope t ∧
        L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ (t + ρ t)))
    (hlocal : ∀ t ∈ Set.Icc a b, ∀ μ : ℝ, |μ - t| < ρ t →
      ApproximatesAtMinimum (Γ t) a b μ E) :
    ∃ Λ : Finset (Label d), Λ.Nonempty ∧
…

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

theorem OAI.Problem326.Affine.exists_approximating_family_of_local_certificates line 273

Source documentation

Choice-packaged form of the gluing theorem: local constructors may return the radius and finite family existentially, and only for centers in the cube.

theorem exists_approximating_family_of_local_certificates {d : ℕ} (hd : 0 < d)
    {a b : ℝ} (hab : a ≤ b) (E : (Fin d → ℝ) → ℝ)
    (hcert : ∀ t ∈ Set.Icc a b, ∃ ρ : ℝ, 0 < ρ ∧
      ∃ Γ : Finset (Label d),
        (⟨fun _ => t, fun _ => 0⟩ : Label d) ∈ Γ ∧
        (∀ L ∈ Γ, Cube a b L.slope ∧ HasMinimum L.slope t ∧
          L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ (t + ρ))) ∧
        (∀ μ : ℝ, |μ - t| < ρ → ApproximatesAtMinimum Γ a b μ E)) :
    ∃ Λ : Finset (Label d), Λ.Nonempty ∧
      (∀ L ∈ Λ, Cube a b L.slope ∧
        L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ a)) ∧
      Approximates Λ a b E := by
…

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