OAI/Analysis/SeparableQuotients/PerturbationOperator.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.Norming.Family.at line 9
  2. lemma OAI.SeparableQuotient.Norming.Family.at_index line 12
  3. lemma OAI.SeparableQuotient.Norming.Family.index_at line 13
  4. lemma OAI.SeparableQuotient.Norming.Family.at_injective line 14
  5. lemma OAI.SeparableQuotient.ActualSpace.cachedNormedT2 line 20
  6. def OAI.SeparableQuotient.ActualSpace.labelAnalysis line 33
  7. lemma OAI.SeparableQuotient.ActualSpace.labelAnalysis_apply line 36
  8. lemma OAI.SeparableQuotient.ActualSpace.norm_labelAnalysis_le line 41
  9. def OAI.SeparableQuotient.ActualSpace.familyOperator line 44
  10. lemma OAI.SeparableQuotient.ActualSpace.norm_familyOperator_le line 47
  11. lemma OAI.SeparableQuotient.ActualSpace.labelAnalysis_coordinate_self line 54
  12. lemma OAI.SeparableQuotient.ActualSpace.labelAnalysis_coordinate_other line 62
  13. lemma OAI.SeparableQuotient.ActualSpace.familyOperator_coordinate line 73
  14. def OAI.SeparableQuotient.ActualSpace.tau line 81
  15. lemma OAI.SeparableQuotient.ActualSpace.tau_pos line 82
  16. lemma OAI.SeparableQuotient.ActualSpace.tau_hasSum line 83
  17. lemma OAI.SeparableQuotient.ActualSpace.tau_summable line 87
  18. lemma OAI.SeparableQuotient.ActualSpace.operator_summable line 89
  19. def OAI.SeparableQuotient.ActualSpace.B line 96

    Source documentation

    The CH perturbation operator with norm at most 1/10.

    def B : StrongDual ℝ E →L[ℝ] W := ∑' n, tau n • familyOperator hCH (Family.at n)

    Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.W, OAI.SeparableQuotient.ActualSpace.tau, OAI.SeparableQuotient.ActualSpace.familyOperator

  20. lemma OAI.SeparableQuotient.ActualSpace.norm_B_le line 98
  21. lemma OAI.SeparableQuotient.ActualSpace.B_coordinate line 106
  22. lemma OAI.SeparableQuotient.ActualSpace.pathMap_mem_closed line 141
  23. lemma OAI.SeparableQuotient.ActualSpace.pathCoset_mem_B_predual line 150
  24. lemma OAI.SeparableQuotient.ActualSpace.B_range_mem_predual_closure line 158
  25. def OAI.SeparableQuotient.ActualSpace.familyVector line 174
  26. lemma OAI.SeparableQuotient.ActualSpace.norm_familyVector_le line 177
  27. lemma OAI.SeparableQuotient.ActualSpace.familyVector_pair line 189
  28. lemma OAI.SeparableQuotient.ActualSpace.vector_summable line 194
  29. lemma OAI.SeparableQuotient.ActualSpace.B_adjoint line 202

    Source documentation

    The adjoint perturbation has range in the canonical evaluation image.

    lemma B_adjoint (w : StrongDual ℝ W) :
    ∃ v : E, w.comp (B hCH) = NormedSpace.inclusionInDoubleDual ℝ E v := by
…

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