OAI/Analysis/SeparableQuotients/BlockApproximation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SeparableQuotient.Singular.exists_unit line 9
  2. lemma OAI.SeparableQuotient.ActualSpace.familyP_initial line 25
  3. lemma OAI.SeparableQuotient.ActualSpace.familyP_color line 33
  4. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.initial_fixed line 39
  5. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.color_fixed line 42
  6. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.coordinate_zero_of_cut line 47
  7. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.coordinate_zero_of_color line 52
  8. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.cut_nonempty line 57
  9. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.beyond_finite line 73
  10. def OAI.SeparableQuotient.ActualSpace.blockCrop line 81
  11. lemma OAI.SeparableQuotient.ActualSpace.blockCrop_mem line 87
  12. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.crop_difference_pure line 93
  13. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.crop_difference_mixed line 113
  14. lemma OAI.SeparableQuotient.ActualSpace.exists_crop_approx line 129
  15. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.exists_tail_small line 141
  16. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.crop_error_bound line 178
  17. lemma OAI.SeparableQuotient.ActualSpace.BranchReduction.exists_next_block line 199

    Source documentation

    A unit vector in the reduced subspace can be approximated in any prescribed ordinal and color tail.

    lemma BranchReduction.exists_next_block (β : Γ) (hβ : (β : Cut) < R.cut)
    (l : ℕ) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1/2) :
    ∃ (x : R.H) (v : Γ →₀ ℝ), ‖x‖ = 1 ∧ v ≠ 0 ∧
      (∀ a ∈ v.support, a ∈ (blockCrop R.cut R.family β l).set .mixed) ∧
      ‖(x : E)-norming.includeFinite v‖ < ε := by
…

    Mentions: OAI.SeparableQuotient.ActualSpace.Cut, OAI.SeparableQuotient.ActualSpace.blockCrop, OAI.SeparableQuotient.ActualSpace.E

  18. def OAI.SeparableQuotient.ActualSpace.BlockApprox.error line 230
  19. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.error_pos line 231
  20. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.error_le line 232
  21. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.error_sum line 236
  22. structure OAI.SeparableQuotient.ActualSpace.BlockApprox.State line 242
  23. structure OAI.SeparableQuotient.ActualSpace.BlockApprox.Step line 247
  24. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.exists_step line 258
  25. def OAI.SeparableQuotient.ActualSpace.BlockApprox.step line 264
  26. def OAI.SeparableQuotient.ActualSpace.BlockApprox.nextState line 266
  27. def OAI.SeparableQuotient.ActualSpace.BlockApprox.state line 271
  28. def OAI.SeparableQuotient.ActualSpace.BlockApprox.node line 275
  29. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.state_ordinal_strict line 277
  30. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.state_color_mono line 284
  31. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.support_after line 289
  32. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.support_color_next line 297
  33. def OAI.SeparableQuotient.ActualSpace.BlockApprox.blocks line 303

    Source documentation

    A block sequence approximating unit vectors in the reduced closed subspace, in the selected pure or mixed family.

    def blocks : BlockSequence R.family where
…

    Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence

  34. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.blocks_norm line 317
  35. lemma OAI.SeparableQuotient.ActualSpace.BlockApprox.blocks_below line 327