OAI/Analysis/ForestSpace/ModulusProofs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ForestSpace.cofinite_nontrivial line 20
2. theorem OAI.ForestSpace.cofinite_exists_unit line 30
3. theorem OAI.ForestSpace.cofiniteKernel line 36
4. theorem OAI.ForestSpace.averageValues_nonempty line 41
5. theorem OAI.ForestSpace.averageValues_bddBelow line 46
6. theorem OAI.ForestSpace.averageInner_le line 52
7. theorem OAI.ForestSpace.averageCenter_bddAbove line 63
8. theorem OAI.ForestSpace.averageModulus_lower_of_subspaces line 70

   Source documentation

   A quantitative subspace formulation implies the literal inf-sup-inf bound. The nonempty-inner-sphere and bounded-supremum details are explicit.

    theorem averageModulus_lower_of_subspaces (hI : ¬FiniteDimensional ℝ E)
       {t L : ℝ} (ht : 0 ≤ t)
       (h : ∀ x : E, ‖x‖ = 1 → ∀ ε : ℝ, 0 < ε → ∃ F : Cofinite E,
         ∀ y : E, y ∈ F.val → ‖y‖ = 1 → L-ε ≤ (‖x+t•y‖+‖x-t•y‖)/2-1) :
       L ≤ averageModulus E norm t := by
   …

   Mentions: OAI.ForestSpace.Cofinite, OAI.ForestSpace.averageModulus

9. theorem OAI.ForestSpace.sqrt_perturbation line 98
10. theorem OAI.ForestSpace.pair_perturbation line 107
11. theorem OAI.ForestSpace.forest_average_head line 129
12. theorem OAI.ForestSpace.forest_average_modulus line 146

    Source documentation

    The midpoint bound for every coordinate-completion forest, using the averaged signed excess rather than its maximum.

     theorem forest_average_modulus [Infinite V]
        (hF : ForestOrder V) (hAnc : ∀ v : V, (Set.Iic v).Finite)
        (t : ℝ) (ht : 0 < t) :
        Real.sqrt (1+t^2/12)-1 ≤ averageModulus (X V) norm t := by
    …

    Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.averageModulus, OAI.ForestSpace.X