AffineLayers.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.Affine.ApproximatesOnSupport line 12
Source documentation
The lower-dimensional induction hypothesis, transported to one support.
```
def ApproximatesOnSupport {d : ℕ} (F : Finset (Label d)) (L : Label d)
    (U : Finset (Fin d)) (t b β : ℝ) (E : (Fin d → ℝ) → ℝ) : Prop :=
…
```
Mentions: OAI.Problem326.Affine.Label
structure OAI.Problem326.Affine.LayerCertificate line 24
Source documentation
Exactly the information needed from one recursively constructed type family. The zero type is the constant baseline; positive types have normalized offset -1. No continuity of offsets or tolerances is assumed.
```
structure LayerCertificate {d : ℕ} (t b : ℝ) (E : (Fin d → ℝ) → ℝ)
    (k : ℕ) (β : ℝ) (F : Finset (Label d)) : Prop where
…
```
Mentions: OAI.Problem326.Affine.Label
def OAI.Problem326.Affine.baselineLabel line 38
lemma OAI.Problem326.Affine.baseline_layer_certificate line 40
lemma OAI.Problem326.Affine.relativeValue_le_iff line 63
lemma OAI.Problem326.Affine.relativeValue_baseline line 72
def OAI.Problem326.Affine.layerUnion line 78
Source documentation
The union of all types, numbered from zero through d - 1.
```
def layerUnion (d : ℕ) (F : ℕ → Finset (Label d)) : Finset (Label d) := by
…
```
Mentions: OAI.Problem326.Affine.Label
lemma OAI.Problem326.Affine.subset_layerUnion line 82
theorem OAI.Problem326.Affine.layerUnion_approximatesAtMinimum line 88

lemma OAI.Problem326.Affine.offset_isLittleO_of_normalized_limit line 163

Source documentation

A normalized leading power is negligible relative to each strictly lower power. This yields the stronger local offset decay, not merely decay at t.

lemma offset_isLittleO_of_normalized_limit {c : ℝ → ℝ} {β q A : ℝ}
    (hqβ : q < β)
    (hc : Tendsto (fun h : ℝ => c h / h ^ β) (𝓝[>] (0 : ℝ)) (𝓝 A)) :
    Asymptotics.IsLittleO (𝓝[>] (0 : ℝ)) c (fun h : ℝ => h ^ q) := by
…

theorem OAI.Problem326.Affine.exists_fixed_minimum_family_of_layers line 188

Source documentation

The actual finite dependent construction at one fixed minimum, separated from the lower-dimensional embedding used to produce each positive-type layer. The returned decay has a strictly higher exponent than t, allowing localization.

theorem exists_fixed_minimum_family_of_layers {d : ℕ} (hd : 0 < d)
    {a t b : ℝ} (htb : t < b) (E : (Fin d → ℝ) → ℝ)
    (hE₀ : 0 < E (fun _ => t))
    (hmake : ∀ k : ℕ, 0 < k → k < d → ∀ β : ℝ, t < β → β < b →
      ∃ F : Finset (Label d), LayerCertificate t b E k β F) :
    ∃ Λ : Finset (Label d), baselineLabel d t ∈ Λ ∧
      ApproximatesAtMinimum Λ a b t E ∧
      ∀ L ∈ Λ, Cube t b L.slope ∧ HasMinimum L.slope t ∧
        ∃ q : ℝ, t < q ∧
          Asymptotics.IsLittleO (𝓝[>] (0 : ℝ)) L.offset (fun h : ℝ => h ^ q) := by
…

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