OAI/Analysis/DiamondDistortion/EquivalentNorm.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DiamondDistortion.EquivalentNorm.Data line 17
  2. lemma OAI.DiamondDistortion.EquivalentNorm.Data.separates line 25
  3. def OAI.DiamondDistortion.EquivalentNorm.Data.Space line 30
  4. instance OAI.DiamondDistortion.EquivalentNorm.Data.(instance at line 31) line 31
  5. instance OAI.DiamondDistortion.EquivalentNorm.Data.(instance at line 32) line 32
  6. instance OAI.DiamondDistortion.EquivalentNorm.Data.(instance at line 33) line 33
  7. instance OAI.DiamondDistortion.EquivalentNorm.Data.(instance at line 35) line 35
  8. def OAI.DiamondDistortion.EquivalentNorm.Data.of line 38
  9. def OAI.DiamondDistortion.EquivalentNorm.Data.val line 39
  10. lemma OAI.DiamondDistortion.EquivalentNorm.Data.norm_of line 40
  11. def OAI.DiamondDistortion.EquivalentNorm.Data.algebraEquiv line 42
  12. def OAI.DiamondDistortion.EquivalentNorm.Data.equiv line 43
  13. lemma OAI.DiamondDistortion.EquivalentNorm.Data.equiv_apply line 45
  14. lemma OAI.DiamondDistortion.EquivalentNorm.Data.equiv_symm_apply line 46
  15. def OAI.DiamondDistortion.EquivalentNorm.Data.uniformEquiv line 47
  16. instance OAI.DiamondDistortion.EquivalentNorm.Data.(instance at line 51) line 51
  17. lemma OAI.DiamondDistortion.PathModel.quadratic_l2 line 58
  18. def OAI.DiamondDistortion.PathModel.linearFullData line 76

    Source documentation

    The original underlying ℓ² space endowed with its literal infimal path cost.

    def linearFullData (h : ℕ) : EquivalentNorm.Data (L2 h) where
…

    Mentions: OAI.DiamondDistortion.EquivalentNorm.Data, OAI.DiamondDistortion.PathModel.L2

  19. def OAI.DiamondDistortion.PathModel.quadraticFullData line 82
  20. abbrev OAI.DiamondDistortion.PathModel.LinearComponent line 89
  21. abbrev OAI.DiamondDistortion.PathModel.QuadraticComponent line 90
  22. abbrev OAI.DiamondDistortion.PathModel.FullLinearSpace line 91
  23. abbrev OAI.DiamondDistortion.PathModel.FullQuadraticSpace line 92
  24. def OAI.DiamondDistortion.CoordinateCompletion.Data.finiteIsometry line 99
  25. def OAI.DiamondDistortion.CoordinateCompletion.Data.completionMap line 103
  26. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.completionMap_coe line 105
  27. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.completionMap_norm line 109
  28. def OAI.DiamondDistortion.CoordinateCompletion.Data.completionIsometry line 115
  29. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.completionMap_surjective line 118
  30. def OAI.DiamondDistortion.CoordinateCompletion.Data.completionEquiv line 129
  31. def OAI.DiamondDistortion.RecursiveModel.outerEmbedding line 137

    Source documentation

    The actual outer Hilbert sum of the component embeddings.

    def outerEmbedding (j : ∀ h,Vec (h+1) →ₗ[ℝ] E h) : ForestVec →ₗ[ℝ] lp E 2 where
…

    Mentions: OAI.DiamondDistortion.RecursiveModel.Vec, OAI.DiamondDistortion.RecursiveModel.ForestVec

  32. lemma OAI.DiamondDistortion.RecursiveModel.outerEmbedding_apply line 147
  33. lemma OAI.DiamondDistortion.RecursiveModel.outerEmbedding_norm line 149
  34. lemma OAI.DiamondDistortion.RecursiveModel.outerEmbedding_single line 157
  35. lemma OAI.DiamondDistortion.RecursiveModel.outerEmbedding_dense line 165
  36. def OAI.DiamondDistortion.FiniteLpDensity.embedding line 185
  37. lemma OAI.DiamondDistortion.FiniteLpDensity.dense line 189
  38. def OAI.DiamondDistortion.EquivalentNorm.Data.coordinateEmbedding line 206
  39. lemma OAI.DiamondDistortion.EquivalentNorm.Data.coordinateEmbedding_norm line 208
  40. lemma OAI.DiamondDistortion.EquivalentNorm.Data.coordinateEmbedding_dense line 210
  41. def OAI.DiamondDistortion.PathModel.linearFullEmbedding line 221
  42. def OAI.DiamondDistortion.PathModel.quadraticFullEmbedding line 223
  43. lemma OAI.DiamondDistortion.PathModel.linearFullEmbedding_norm line 225
  44. lemma OAI.DiamondDistortion.PathModel.quadraticFullEmbedding_norm line 227
  45. lemma OAI.DiamondDistortion.PathModel.linearFullEmbedding_dense line 229
  46. lemma OAI.DiamondDistortion.PathModel.quadraticFullEmbedding_dense line 231
  47. def OAI.DiamondDistortion.PathModel.linearFullEquiv line 234
  48. def OAI.DiamondDistortion.PathModel.quadraticFullEquiv line 236
  49. lemma OAI.DiamondDistortion.PathModel.linearFullEquiv_embedding line 238
  50. lemma OAI.DiamondDistortion.PathModel.quadraticFullEquiv_embedding line 240
  51. def OAI.DiamondDistortion.LpBoundedMap.normVector line 248
  52. lemma OAI.DiamondDistortion.LpBoundedMap.normVector_norm line 250
  53. def OAI.DiamondDistortion.LpBoundedMap.map line 253
  54. lemma OAI.DiamondDistortion.LpBoundedMap.map_apply line 258
  55. lemma OAI.DiamondDistortion.LpBoundedMap.map_norm line 260