OAI/Analysis/TriangularHilbert/Quantization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularHilbert.measurable_gridIndex line 13
  2. lemma OAI.TriangularHilbert.measurable_gridPoint line 16
  3. def OAI.TriangularHilbert.gridSquare line 19
  4. lemma OAI.TriangularHilbert.measurable_gridSquare line 21
  5. lemma OAI.TriangularHilbert.tendsto_gridPoint line 24
  6. lemma OAI.TriangularHilbert.tendsto_gridSquare line 30
  7. def OAI.TriangularHilbert.sampleIndices line 34
  8. lemma OAI.TriangularHilbert.mem_sampleIndices line 36
  9. def OAI.TriangularHilbert.sampledMatrix line 47
  10. lemma OAI.TriangularHilbert.gridLift_sampled line 50
  11. lemma OAI.TriangularHilbert.sampled_support line 63