FixedMinimumCertificate.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.Affine.constantLabel line 14
Source documentation
The unshifted constant-slope label used at a fixed minimum level.
```
def constantLabel (d : ℕ) (t : ℝ) : Label d :=
…
```
Mentions: OAI.Problem326.Affine.Label
structure OAI.Problem326.Affine.FixedMinimumLabelCertificate line 20
Source documentation
Finite construction data for one label. The inner_bound field is exactly what the lower-dimensional induction supplies after restricting activity to the lifted family. All remaining fields concern finite choices or offset asymptotics.
```
structure FixedMinimumLabelCertificate {d : ℕ} (Λ : Finset (Label d))
    (a b t : ℝ) (E : (Fin d → ℝ) → ℝ) (L : Label d) where
…
```
Mentions: OAI.Problem326.Affine.Label
lemma OAI.Problem326.Affine.relativeValue_eq_value_sub line 44
lemma OAI.Problem326.Affine.active_relativeValue_le line 52
theorem OAI.Problem326.Affine.approximatesAtMinimum_of_certificates line 60
theorem OAI.Problem326.Affine.normalized_shifted_offset line 103

theorem OAI.Problem326.Affine.offset_isLittleO_of_normalized line 118

Source documentation

A normalized type offset decays faster than every smaller power.

theorem offset_isLittleO_of_normalized {c : ℝ → ℝ} {s β : ℝ}
    (hc : Tendsto (fun h : ℝ => c h / h ^ β) (𝓝[>] 0) (𝓝 (-1)))
    (hsβ : s < β) : c =o[𝓝[>] 0] (fun h : ℝ => h ^ s) := by
…

theorem OAI.Problem326.Affine.exists_common_offset_decay line 141
Source documentation
Finitely many type certificates have one common exponent strictly above the fixed minimum at which all their offsets are little-o. This decay allows localization and inter-family gluing.
```
theorem exists_common_offset_decay {d : ℕ}
    {Λ : Finset (Label d)} {a b t : ℝ} {E : (Fin d → ℝ) → ℝ}
    (hcert : ∀ L ∈ Λ, FixedMinimumLabelCertificate Λ a b t E L) :
    ∃ s : ℝ, t < s ∧ ∀ L ∈ Λ, L.offset =o[𝓝[>] 0] (fun h : ℝ => h ^ s) := by
…
```
Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.FixedMinimumLabelCertificate