OAI/Analysis/SeparableQuotients/BranchSeparation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.blockProjection_embed line 12
2. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.coefficient_bound line 28
3. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.finite_perturbation line 54

   Source documentation

   The small-perturbation inequality for finite block combinations.

   lemma BlockSequence.finite_perturbation (hz : ∀ n, (1/2 : ℝ) ≤ ‖z.embed n‖)
       (h : ℕ → E) (ε : ℕ → ℝ) (_hε : ∀ n, 0 ≤ ε n)
       (he : ∀ n, ‖h n-z.embed n‖ ≤ ε n) (B : ℝ)
       (hs : ∀ s : Finset ℕ, ∑ n ∈ s, ε n ≤ B) (c : ℕ →₀ ℝ) :
       ‖c.sum (fun i a => a • h i) - c.sum (fun i a => a • z.embed i)‖ ≤
         (4*B)*‖c.sum (fun i a => a • z.embed i)‖ := by
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.B

4. lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_familyP line 83
5. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.pair_below line 98
6. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.pair_color line 114
7. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.pathPartial_familyP line 123
8. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.pathFunctional_familyP line 134
9. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.pair_coefficients line 140
10. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.pair_approximation line 151
11. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.separated_on_reduction line 171
12. theorem OAI.SeparableQuotient.ActualSpace.BlockApprox.restricted_separated line 196

    Source documentation

    Uniformly separated path restrictions on an arbitrary closed infinite-dimensional subspace.

    theorem restricted_separated {b c : ℕ → Bool} (hbc : b ≠ c) :
        (1/(2004*(‖R.U‖+1)) : ℝ) ≤
          ‖(pathFunctional (TreeNode.branchPath (blocks R) b)).comp F.subtypeL -
            (pathFunctional (TreeNode.branchPath (blocks R) c)).comp F.subtypeL‖ := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.pathFunctional, OAI.SeparableQuotient.ActualSpace.TreeNode.branchPath, OAI.SeparableQuotient.ActualSpace.BlockApprox.blocks