OAI/Analysis/TreePotential/CostObstruction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreePotentials.subspace_radial_adjustment line 13
2. lemma OAI.BoundedTreePotentials.oneSided_growth_boundary line 39

   Source documentation

   Boundary radius is allowed: correcting a quotient approximant radially costs at most twice its approximation error.

   lemma oneSided_growth_boundary {t γ c : ℝ} (ht : 0 < t) (hγ : 0 < γ)
       (hδ : (γ : EReal) < oneSidedModulus E t) (p : E) (hp : 0 < ‖p‖)
       (htp : t * ‖p‖ ≤ c) (d : ℕ → E) (hd : WeaklyNull d)
       (hdn : ∀ n, c ≤ ‖d n‖) :
       ∃ n, ‖p‖ + γ * ‖p‖ / 2 ≤ ‖p + d n‖ := by
   …

   Mentions: OAI.BoundedTreePotentials.oneSidedModulus, OAI.BoundedTreePotentials.WeaklyNull

3. theorem OAI.BoundedTreePotentials.bounded_tree_modulus_eq_zero_le line 56
4. lemma OAI.BoundedTreePotentials.prefix_child_iff line 113
5. lemma OAI.BoundedTreePotentials.rootPath_child line 118
6. lemma OAI.BoundedTreePotentials.single_sequence_weaklyNull line 137
7. def OAI.BoundedTreePotentials.raiseTree line 148
8. lemma OAI.BoundedTreePotentials.raiseTree_child line 149
9. def OAI.BoundedTreePotentials.linearOuterInsert line 152
10. def OAI.BoundedTreePotentials.linearOuterTree line 155
11. lemma OAI.BoundedTreePotentials.linearOuterTree_difference line 158
12. lemma OAI.BoundedTreePotentials.linearOuterTree_weak line 164
13. lemma OAI.BoundedTreePotentials.linearOuterTree_norm line 174
14. lemma OAI.BoundedTreePotentials.linearOuterTree_increment line 180
15. def OAI.BoundedTreePotentials.quadraticOuterInsert line 187
16. def OAI.BoundedTreePotentials.quadraticOuterTree line 190
17. lemma OAI.BoundedTreePotentials.quadraticOuterTree_difference line 193
18. lemma OAI.BoundedTreePotentials.quadraticOuterTree_weak line 199
19. lemma OAI.BoundedTreePotentials.quadraticOuterTree_norm line 209
20. lemma OAI.BoundedTreePotentials.quadraticOuterTree_increment line 215
21. theorem OAI.BoundedTreePotentials.linearOuter_renorming_obstruction line 228

    Source documentation

    The boundary radius alpha/beta is included.

    theorem linearOuter_renorming_obstruction (e : LinearOuter ≃L[ℝ] Y) {α β t : ℝ}
        (hα : 0 < α) (hαβ : α ≤ β)
        (he : ∀ x, α * ‖x‖ ≤ ‖e x‖ ∧ ‖e x‖ ≤ β * ‖x‖)
        (ht : 0 < t) (htb : t ≤ α/β) : oneSidedModulus Y t = 0 := by
    …

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.oneSidedModulus

22. theorem OAI.BoundedTreePotentials.quadraticOuter_renorming_obstruction line 244
23. theorem OAI.BoundedTreePotentials.linearOuter_no_equivalent_AUC line 274
24. theorem OAI.BoundedTreePotentials.quadraticOuter_no_equivalent_AUC line 282