OAI/Analysis/DiamondDistortion/CoordinateSpace.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DiamondDistortion.CoordinateCompletion.Data line 18

    Source documentation

    A specified coordinate norm, with individually bounded coordinate evaluations. No bound on the norms of coordinate projections is imposed.

    structure Data (ι : Type*) where
…
  2. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.separates line 24
  3. def OAI.DiamondDistortion.CoordinateCompletion.Data.Finite line 31
  4. instance OAI.DiamondDistortion.CoordinateCompletion.Data.(instance at line 32) line 32
  5. instance OAI.DiamondDistortion.CoordinateCompletion.Data.(instance at line 33) line 33
  6. instance OAI.DiamondDistortion.CoordinateCompletion.Data.(instance at line 34) line 34
  7. instance OAI.DiamondDistortion.CoordinateCompletion.Data.(instance at line 36) line 36
  8. abbrev OAI.DiamondDistortion.CoordinateCompletion.Data.Space line 38
  9. def OAI.DiamondDistortion.CoordinateCompletion.Data.finite line 40
  10. def OAI.DiamondDistortion.CoordinateCompletion.Data.array line 41
  11. def OAI.DiamondDistortion.CoordinateCompletion.Data.embedding line 42
  12. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.norm_embedding line 44
  13. def OAI.DiamondDistortion.CoordinateCompletion.Data.coordinateFinite line 47
  14. def OAI.DiamondDistortion.CoordinateCompletion.Data.coordinate line 53
  15. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.coordinate_coe line 55
  16. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.coordinate_embedding line 58
  17. def OAI.DiamondDistortion.CoordinateCompletion.Data.unit line 60
  18. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.coordinate_unit line 61
  19. def OAI.DiamondDistortion.CoordinateCompletion.Data.projection line 64
  20. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_apply line 66
  21. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.coordinate_projection line 68
  22. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_idempotent line 71
  23. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_commutes line 79
  24. def OAI.DiamondDistortion.CoordinateCompletion.Data.headMap line 89
  25. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_range line 93
  26. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_finite line 101
  27. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_embedding line 105
  28. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.finite_fixed line 115
  29. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.approximation line 125
  30. def OAI.DiamondDistortion.CoordinateCompletion.Data.heads line 138
  31. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.heads_commutes line 146
  32. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.projection_eq_embedding line 152

    Source documentation

    Every vector fixed by a finite head is an actual finite coordinate vector.

    lemma projection_eq_embedding (H : Finset ι) (x : A.Space) :
    ∃ v : ι →₀ ℝ,A.projection H x=A.embedding v := by
…
  33. lemma OAI.DiamondDistortion.CoordinateCompletion.Data.fixed_finite line 157