OAI/Analysis/ForestSpace/Renorming.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForestSpace.WeakNull line 18

   Source documentation

   Weak convergence against the entire continuous dual.

   def WeakNull (d : ℕ → E) : Prop :=
   …

2. theorem OAI.ForestSpace.weakNull_finiteDimensional line 21
3. theorem OAI.ForestSpace.weakNull_cofinite_approx line 32
4. theorem OAI.ForestSpace.EquivalentNorm.beta_pos line 57
5. theorem OAI.ForestSpace.EquivalentNorm.nonneg line 58
6. theorem OAI.ForestSpace.EquivalentNorm.pos line 60
7. theorem OAI.ForestSpace.EquivalentNorm.continuous line 63
8. theorem OAI.ForestSpace.EquivalentNorm.cofinite_unit line 70
9. theorem OAI.ForestSpace.EquivalentNorm.support line 77
10. theorem OAI.ForestSpace.EquivalentNorm.aucValues_nonempty line 99
11. theorem OAI.ForestSpace.EquivalentNorm.aucValues_bddBelow line 104
12. theorem OAI.ForestSpace.EquivalentNorm.aucInner_le line 110
13. theorem OAI.ForestSpace.EquivalentNorm.aucCenter_bddAbove line 120
14. theorem OAI.ForestSpace.EquivalentNorm.aucCenter_nonneg line 125
15. theorem OAI.ForestSpace.EquivalentNorm.aucModulus_nonneg line 139
16. theorem OAI.ForestSpace.EquivalentNorm.aucModulus_le_center line 147
17. theorem OAI.ForestSpace.EquivalentNorm.subspace_gain line 154
18. theorem OAI.ForestSpace.EquivalentNorm.gain_extended line 174
19. theorem OAI.ForestSpace.EquivalentNorm.vector_gain line 198
20. theorem OAI.ForestSpace.EquivalentNorm.child_gain line 215
21. theorem OAI.ForestSpace.EquivalentNorm.bounded_trees_auc_zero line 259

    Source documentation

    The obstruction scale for bounded norm-one paths and norm-one (or larger) weakly null child increments. An additive form of the uniform gain is enough for the final finite-height contradiction.

     theorem EquivalentNorm.bounded_trees_auc_zero (hI : ¬FiniteDimensional ℝ E)
        (u : ℕ → List ℕ → E)
        (hu : ∀ h ≥ 1, ∀ s : List ℕ, s.length ≤ h → ‖u h s‖ = 1)
        (hd : ∀ h ≥ 1, ∀ s : List ℕ, s.length < h → ∀ j,
          1 ≤ ‖u h (s++[j])-u h s‖)
        (hweak : ∀ h ≥ 1, ∀ s : List ℕ, s.length < h →
          WeakNull (fun j => u h (s++[j])-u h s)) :
        aucModulus E R.N (α/(2*β)) = 0 := by
    …

    Mentions: OAI.ForestSpace.WeakNull, OAI.ForestSpace.aucModulus