OAI/Analysis/DiamondDistortion/GraphBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DiamondDistortion.forest_normer_first line 16

   Source documentation

   Exact positive-rho qualitative result for the complete finite-forest dual.

   theorem forest_normer_first {ε : ℝ} (hε : 0 < ε) :
       ∃ ρ : ℝ,0 < ρ ∧ ρ < 1 ∧ Diamond.UnitLensBound ForestDual ε ρ :=
   …

   Mentions: OAI.DiamondDistortion.Diamond.UnitLensBound, OAI.DiamondDistortion.ForestDual

2. theorem OAI.DiamondDistortion.forest_qualitative_backward line 20
3. theorem OAI.DiamondDistortion.forest_radial_deficit line 35

   Source documentation

   The separately stated exact radial constant C_* = sqrt 2 + sqrt 6. The proof uses the stronger established bound on the identical norm.

   theorem forest_radial_deficit {D s : ℝ} (k : ℕ) (f : Diamond.Vertex k → ForestDual)
       (hf : Diamond.HasDistortion k f D s) :
       (k:ℝ) ≤ (Real.sqrt 2+Real.sqrt 6)^2*D*(D-1) := by
   …

   Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.ForestDual, OAI.DiamondDistortion.Diamond.HasDistortion

4. theorem OAI.DiamondDistortion.Midpoint.Heads.vanishing_lens_pos line 52
5. lemma OAI.DiamondDistortion.DirectLayers.Regular.transport line 62
6. instance OAI.DiamondDistortion.PathModel.linearFullDualSeparable line 79
7. theorem OAI.DiamondDistortion.PathModel.linear_full_weak_graph line 83
8. theorem OAI.DiamondDistortion.PathModel.linear_full_regular line 87
9. theorem OAI.DiamondDistortion.PathModel.full_adaptive_graph line 89
10. theorem OAI.DiamondDistortion.PathModel.full_predictable_495_graph line 96
11. theorem OAI.DiamondDistortion.PathModel.full_variation_252_graph line 101
12. theorem OAI.DiamondDistortion.PathModel.full_leakage_1024_graph line 106
13. theorem OAI.DiamondDistortion.PathModel.full_squared_gap_400_graph line 113
14. theorem OAI.DiamondDistortion.RecursiveModel.full_cubic_weak line 127

    Source documentation

    The weak-null clause on the literal full ℓ_p recursive-array model.

    theorem full_cubic_weak (hinput : CubicInput fullVectorHeads) {ε : ℝ}
        (hε : 0 < ε) (hε1 : ε ≤ 1) (x : FullVectorSpace) (z : ℕ → FullVectorSpace)
        (hz : Midpoint.WeaklyNull z) (hl : ∀ i,ε ≤ ‖z i‖)
        (hp : ∀ i,‖x+z i‖ ≤ 1) (hm : ∀ i,‖x-z i‖ ≤ 1) : ‖x‖ ≤ theta ε :=
    …

    Mentions: OAI.DiamondDistortion.RecursiveModel.fullVectorHeads, OAI.DiamondDistortion.RecursiveModel.FullVectorSpace, OAI.DiamondDistortion.Midpoint.WeaklyNull

15. theorem OAI.DiamondDistortion.RecursiveModel.full_sixth_lens line 134

    Source documentation

    The infinite separated-lens clause, before the graph specialization.

    theorem full_sixth_lens (hinput : SixthInput fullVectorHeads) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
        Diamond.UnitLensBound FullVectorSpace ε (q6 ε) :=
    …

    Mentions: OAI.DiamondDistortion.RecursiveModel.fullVectorHeads, OAI.DiamondDistortion.Diamond.UnitLensBound, OAI.DiamondDistortion.RecursiveModel.FullVectorSpace