TypeFamilyCertificate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.typeFamily_approximatesOnSupport line 16
Source documentation
Project the full lower-dimensional approximation certificate into a member of the injection-indexed type family. The approximating exponents need not stay in any cube.
```
theorem typeFamily_approximatesOnSupport {k d : ℕ} (t β b : ℝ)
    (E : (Fin d → ℝ) → ℝ)
    (C : ∀ e : Fin k ↪ Fin d,
      FullCertificate k β b (fun s => E (embedCoordinates e t s)))
    (e : Fin k ↪ Fin d) {L : Label k} (hL : L ∈ (C e).labels) :
    ApproximatesOnSupport
      (typeFamily t β (fun e => (C e).labels)) (L.embed e t β)
      (Finset.univ.map e) t b β E := by
…
```
Mentions: OAI.Problem326.Affine.FullCertificate, OAI.Problem326.Affine.embedCoordinates, OAI.Problem326.Affine.Label, OAI.Problem326.Affine.ApproximatesOnSupport, OAI.Problem326.Affine.typeFamily
theorem OAI.Problem326.Affine.typeFamily_layerCertificate line 40
Source documentation
The actual positive-type constructor: lower-dimensional full certificates for every coordinate injection produce the exact layer certificate consumed by fixed-minimum assembly.
```
theorem typeFamily_layerCertificate {k d : ℕ} (hk : 0 < k)
    {t β b : ℝ} (htβ : t < β) (hβb : β < b)
    (E : (Fin d → ℝ) → ℝ)
    (hE : ∀ r, Cube t b r → 0 < E r)
    (C : ∀ e : Fin k ↪ Fin d,
      FullCertificate k β b (fun s => E (embedCoordinates e t s))) :
    LayerCertificate t b E k β (typeFamily t β (fun e => (C e).labels)) := by
…
```
Mentions: OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.FullCertificate, OAI.Problem326.Affine.embedCoordinates, OAI.Problem326.Affine.LayerCertificate, OAI.Problem326.Affine.typeFamily

theorem OAI.Problem326.Affine.exists_typeFamily_layerCertificate line 74

Source documentation

The per-layer existence interface used by the finite threshold recursion. The only input is the lower-dimensional full approximation theorem.

theorem exists_typeFamily_layerCertificate {k d : ℕ}
    (hk : 0 < k) (hkd : k < d) {t β b : ℝ}
    (htβ : t < β) (hβb : β < b)
    (E : (Fin d → ℝ) → ℝ)
    (hE : ∀ r, Cube t b r → 0 < E r)
    (hIH : ∀ E' : (Fin k → ℝ) → ℝ,
      (∀ s, Cube β b s → 0 < E' s) → Nonempty (FullCertificate k β b E')) :
    ∃ F : Finset (Label d), F.Nonempty ∧ LayerCertificate t b E k β F := by
…

Mentions: OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.FullCertificate, OAI.Problem326.Affine.Label, OAI.Problem326.Affine.LayerCertificate