OAI/Analysis/TreePotential/SegmentComponents.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.Segments.componentSlice line 13
  2. def OAI.BoundedTreePotentials.Segments.componentPart line 16
  3. lemma OAI.BoundedTreePotentials.Segments.slice_apply line 19
  4. lemma OAI.BoundedTreePotentials.Segments.componentPart_apply line 22
  5. lemma OAI.BoundedTreePotentials.Segments.componentPart_eq line 25
  6. lemma OAI.BoundedTreePotentials.Segments.componentNorm line 40
  7. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_component line 44
  8. lemma OAI.BoundedTreePotentials.Segments.predual_family_energy line 57
  9. lemma OAI.BoundedTreePotentials.Segments.predual_norm_le_of_energy line 63
  10. lemma OAI.BoundedTreePotentials.Segments.Incomparable.subset line 78
  11. lemma OAI.BoundedTreePotentials.Segments.component_families_incomparable line 81
  12. lemma OAI.BoundedTreePotentials.Segments.component_families_disjoint line 93
  13. lemma OAI.BoundedTreePotentials.Segments.component_family_energy_sum line 100
  14. lemma OAI.BoundedTreePotentials.Segments.component_family_energy line 106
  15. lemma OAI.BoundedTreePotentials.Segments.eval_zero_outside_components line 114
  16. lemma OAI.BoundedTreePotentials.Segments.predual_norm_sq_le_components line 122
  17. def OAI.BoundedTreePotentials.Segments.Atom.component line 147
  18. lemma OAI.BoundedTreePotentials.Segments.Atom.component_pairing line 153
  19. lemma OAI.BoundedTreePotentials.Segments.Atom.pairing_sq_le_energy line 157
  20. lemma OAI.BoundedTreePotentials.Segments.component_atom_pairings_sq line 164
  21. lemma OAI.BoundedTreePotentials.Segments.exists_atom_near_norm line 174
  22. lemma OAI.BoundedTreePotentials.Segments.components_norm_sq_le_predual line 182
  23. theorem OAI.BoundedTreePotentials.Segments.predual_components_norm_sq line 214

    Source documentation

    Exact finite-array orthogonal sum identity, with no uniform height bound. All trees retain their heights and their root coordinates.

    theorem predual_components_norm_sq (g : Node →₀ ℝ) (H : Finset ℕ)
    (hg : ∀ v ∈ g.support, v.1 ∈ H) :
    (testNorm atomTests g)^2=∑ n ∈ H, (testNorm (blockTests n) (componentSlice n g))^2 := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.testNorm, OAI.BoundedTreePotentials.Segments.atomTests, OAI.BoundedTreePotentials.Segments.blockTests, OAI.BoundedTreePotentials.Segments.componentSlice

  24. def OAI.BoundedTreePotentials.finiteLift line 224

    Source documentation

    The canonical c00 inclusion, used for each of the exact test families.

    def finiteLift {I : Type*} (K : TestFamily I) : (I →₀ ℝ) →ₗ[ℝ] TestCompletion K :=
…

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.TestCompletion

  25. lemma OAI.BoundedTreePotentials.finiteLift_norm line 227
  26. def OAI.BoundedTreePotentials.Segments.componentSupport line 234
  27. lemma OAI.BoundedTreePotentials.Segments.mem_componentSupport line 236
  28. lemma OAI.BoundedTreePotentials.Segments.slice_zero_outside line 239
  29. lemma OAI.BoundedTreePotentials.Segments.finiteComponents_mem line 246
  30. def OAI.BoundedTreePotentials.Segments.finiteComponents line 256
  31. lemma OAI.BoundedTreePotentials.Segments.finiteComponents_apply line 271
  32. lemma OAI.BoundedTreePotentials.Segments.finiteComponents_norm line 274
  33. def OAI.BoundedTreePotentials.Segments.finiteComponentIsometry line 288
  34. def OAI.BoundedTreePotentials.Segments.completedComponents line 292
  35. lemma OAI.BoundedTreePotentials.Segments.completedComponents_coe line 295
  36. lemma OAI.BoundedTreePotentials.Segments.completedComponents_lift line 300
  37. lemma OAI.BoundedTreePotentials.Segments.completedComponents_norm line 304
  38. def OAI.BoundedTreePotentials.Segments.componentIsometry line 311
  39. lemma OAI.BoundedTreePotentials.Segments.finiteComponents_emb line 315
  40. lemma OAI.BoundedTreePotentials.Segments.completedComponents_surjective line 337
  41. def OAI.BoundedTreePotentials.Segments.predualComponentEquiv line 356

    Source documentation

    Exact ℓ₂ decomposition of the completed predual into completed blocks.

    def predualComponentEquiv : Predual ≃ₗᵢ[ℝ] HilbertSum PredualBlock :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Predual, OAI.BoundedTreePotentials.HilbertSum, OAI.BoundedTreePotentials.Segments.PredualBlock

  42. theorem OAI.BoundedTreePotentials.Segments.predual_reflexive line 359