OAI/Analysis/DiamondDistortion/CoordinateDual.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiamondDistortion.CoordinateCompletion.Data.Dual line 17
  2. def OAI.DiamondDistortion.CoordinateCompletion.Data.dualEmbedding line 19
  3. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualEmbedding_apply line 21
  4. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualEmbedding_embedding line 25
  5. def OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection line 30
  6. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection_apply line 32
  7. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection_unit line 34
  8. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection_idempotent line 38
  9. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection_fixed line 46
  10. def OAI.DiamondDistortion.CoordinateCompletion.Data.dualHeadMap line 57
  11. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection_finite line 61
  12. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.embedding_sum line 72
  13. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.pairing line 77
  14. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.small_color_tail_upper line 82
  15. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.small_color_tail line 149
  16. structure OAI.DiamondDistortion.CoordinateCompletion.Data.HilbertBlocks line 166

    Source documentation

    Orthogonal outer blocks whose finite unions have their actual norm equivalent to coordinate ℓ². Constants may depend on the finite union, not globally.

    structure HilbertBlocks (c : ι → κ) : Prop where
…
  17. def OAI.DiamondDistortion.FiniteCoordinates.array line 182
  18. lemma OAI.DiamondDistortion.FiniteCoordinates.array_apply line 183
  19. lemma OAI.DiamondDistortion.FiniteCoordinates.array_support line 186
  20. lemma OAI.DiamondDistortion.FiniteCoordinates.array_energy line 190
  21. lemma OAI.DiamondDistortion.FiniteCoordinates.filter_energy_le line 202
  22. lemma OAI.DiamondDistortion.FiniteCoordinates.square_tails line 211
  23. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.pairing_array line 227
  24. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualEmbedding_array line 230
  25. def OAI.DiamondDistortion.CoordinateCompletion.Data.coefficients line 237
  26. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.coefficients_bounded line 239
  27. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dual_approximation line 275
  28. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dual_separable line 379
  29. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.dualProjection_commutes line 394