AffineCertificates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Certificates for the dimension induction and interval gluing.

In particular a local certificate retains a strictly stronger offset decay exponent. Merely retaining o(h^t) would not suffice for interval gluing.

def OAI.Problem326.Affine.SequentialApproximation line 18
Source documentation
Sequential approximation on the whole exponent cube, allowing the approximating sequence to lie outside the cube.
```
def SequentialApproximation {d : ℕ} (Λ : Finset (Label d))
    (a b : ℝ) (E : (Fin d → ℝ) → ℝ) : Prop :=
…
```
Mentions: OAI.Problem326.Affine.Label
structure OAI.Problem326.Affine.FullCertificate line 28
Source documentation
The conclusion of the affine approximation lemma in one dimension d. The label set and its slopes are fixed before a small parameter is chosen.
```
structure FullCertificate (d : ℕ) (a b : ℝ) (E : (Fin d → ℝ) → ℝ) where
…
```
structure OAI.Problem326.Affine.LocalCertificate line 38
Source documentation
The output required at a fixed minimum before neighborhood extension. decay_gt and offsets are essential data for the subsequent gluing step.
```
structure LocalCertificate (d : ℕ) (a b t : ℝ) (E : (Fin d → ℝ) → ℝ) where
…
```
lemma OAI.Problem326.Affine.LocalCertificate.nonempty line 49
def OAI.Problem326.Affine.localCertificate_one line 54
Source documentation
The fixed-minimum singleton construction in species dimension one.
```
def localCertificate_one (a b t : ℝ) (htb : t ≤ b)
    (E : (Fin 1 → ℝ) → ℝ) (hE : 0 < E (fun _ => t)) :
    LocalCertificate 1 a b t E := by
…
```
Mentions: OAI.Problem326.Affine.LocalCertificate
def OAI.Problem326.Affine.localCertificate_upper line 82
Source documentation
The fixed-minimum singleton construction at the upper corner.
```
def localCertificate_upper {d : ℕ} (hd : 0 < d) (a b : ℝ)
    (E : (Fin d → ℝ) → ℝ) (hE : 0 < E (fun _ => b)) :
    LocalCertificate d a b b E := by
…
```
Mentions: OAI.Problem326.Affine.LocalCertificate
def OAI.Problem326.Affine.fullCertificate_zero line 111
Source documentation
Harmless dimension-zero base for strong induction. It is not used as a positive-dimensional fixed-minimum family.
```
def fullCertificate_zero (a b : ℝ) (E : (Fin 0 → ℝ) → ℝ)
    (hE : ∀ r, Cube a b r → 0 < E r) : FullCertificate 0 a b E := by
…
```
Mentions: OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.FullCertificate

theorem OAI.Problem326.Affine.fullCertificate_of_local_and_glue line 137

Source documentation

Strong induction assembles full certificates from fixed-minimum certificates and finite interval gluing.

theorem fullCertificate_of_local_and_glue
    (construct : ∀ d : ℕ, 0 < d →
      (∀ k : ℕ, k < d → ∀ a b : ℝ, ∀ E : (Fin k → ℝ) → ℝ,
        a < b → (∀ r, Cube a b r → 0 < E r) → Nonempty (FullCertificate k a b E)) →
      ∀ a b : ℝ, ∀ E : (Fin d → ℝ) → ℝ,
        a < b → (∀ r, Cube a b r → 0 < E r) →
        ∀ t : ℝ, a ≤ t → t ≤ b → Nonempty (LocalCertificate d a b t E))
    (glue : ∀ d : ℕ, 0 < d → ∀ a b : ℝ, ∀ E : (Fin d → ℝ) → ℝ,
      a < b → (∀ r, Cube a b r → 0 < E r) →
      (∀ t : ℝ, a ≤ t → t ≤ b → Nonempty (LocalCertificate d a b t E)) →
      Nonempty (FullCertificate d a b E)) :
    ∀ d : ℕ, ∀ a b : ℝ, ∀ E : (Fin d → ℝ) → ℝ,
…

Mentions: OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.FullCertificate, OAI.Problem326.Affine.LocalCertificate