OAI/Analysis/ForestSpace/Components.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ForestSpace.componentRaw line 15
  2. theorem OAI.ForestSpace.componentRaw_apply line 20
  3. def OAI.ForestSpace.liftComponent line 23
  4. theorem OAI.ForestSpace.liftComponent_apply line 26
  5. theorem OAI.ForestSpace.componentRaw_lift_same line 30
  6. theorem OAI.ForestSpace.componentRaw_lift_other line 35
  7. def OAI.ForestSpace.componentSupport line 41
  8. theorem OAI.ForestSpace.componentRaw_zero line 44
  9. def OAI.ForestSpace.rawDecompositionLinear line 52
  10. theorem OAI.ForestSpace.rawDecomposition_apply line 68
  11. theorem OAI.ForestSpace.rawDecomposition_norm_sq line 71
  12. theorem OAI.ForestSpace.segment_component_subtype line 80
  13. theorem OAI.ForestSpace.segment_component_image line 88
  14. theorem OAI.ForestSpace.segSum_component_image line 101
  15. theorem OAI.ForestSpace.segment_single_height line 105
  16. theorem OAI.ForestSpace.segSum_component_subtype line 110
  17. theorem OAI.ForestSpace.segSum_sq_components line 126
  18. theorem OAI.ForestSpace.norm_le_rawDecomposition line 144
  19. theorem OAI.ForestSpace.exists_half_test line 163
  20. theorem OAI.ForestSpace.rawDecomposition_norm_le line 176
  21. def OAI.ForestSpace.rawDecomposition line 214
  22. theorem OAI.ForestSpace.rawDecomposition_lift line 217
  23. theorem OAI.ForestSpace.rawDecomposition_dense line 225
  24. theorem OAI.ForestSpace.reflexive_forest_J line 243

    Source documentation

    The specified disjoint-component segment completion is canonically reflexive. Only bounded isomorphisms are needed here; its norm is unchanged.

     theorem reflexive_forest_J : Reflexive (J Vertex) := by
…

    Mentions: OAI.ForestSpace.Reflexive, OAI.ForestSpace.J, OAI.ForestSpace.Vertex