OAI/Analysis/RotationWeights/GraphTransfer.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleSampling.graph_restriction_convergence line 67
  2. def OAI.CircleSampling.orbitEquiv line 148
  3. lemma OAI.CircleSampling.orbitEquiv_apply line 149
  4. lemma OAI.CircleSampling.orbitEquiv_symm_apply line 150
  5. lemma OAI.CircleSampling.orbitEquiv_preserving line 152
  6. def OAI.CircleSampling.stageGraph line 154
  7. lemma OAI.CircleSampling.stageGraph_fst line 159
  8. lemma OAI.CircleSampling.stageGraph_snd line 163
  9. def OAI.CircleSampling.translation line 178
  10. lemma OAI.CircleSampling.quotient_norm_le line 179
  11. lemma OAI.CircleSampling.stageGraph_support line 181
  12. lemma OAI.CircleSampling.gridTolerance_bound line 200
  13. lemma OAI.CircleSampling.gridTolerance_tendsto line 213
  14. def OAI.CircleSampling.rationalPoint line 217
  15. def OAI.CircleSampling.rationalIndex line 218
  16. lemma OAI.CircleSampling.rationalIndex_spec line 221
  17. def OAI.CircleSampling.rationalGraph line 225
  18. def OAI.CircleSampling.circleProbability line 228
  19. lemma OAI.CircleSampling.rationalGraph_convergence line 229
  20. theorem OAI.ContinuousCircleWeight.continuousOn_compact_graph line 264
  21. theorem OAI.ContinuousCircleWeight.measurable_lusin_compact line 286
  22. theorem OAI.ContinuousCircleWeight.finiteMeasure_compl_le_of_tendsto line 314
  23. theorem OAI.ContinuousCircleWeight.isCompact_all_zeros line 342
  24. theorem OAI.ContinuousCircleWeight.compact_relation_transfer line 356
  25. lemma OAI.ContinuousCircleWeight.continuous_bounded_field_apply line 398
  26. def OAI.ContinuousCircleWeight.cappedRatio line 416
  27. lemma OAI.ContinuousCircleWeight.cappedRatio_bounds line 419
  28. def OAI.ContinuousCircleWeight.cappedDiagonal line 423
  29. lemma OAI.ContinuousCircleWeight.continuous_cappedDiagonal line 428
  30. instance OAI.ContinuousCircleWeight.fiberSeparable line 450
  31. def OAI.ContinuousCircleWeight.cappedPairRelation line 460
  32. lemma OAI.ContinuousCircleWeight.cappedPairRelation_iff line 464
  33. lemma OAI.ContinuousCircleWeight.cappedPairRelation_compact_approx line 483
  34. theorem OAI.ContinuousCircleWeight.capped_pair_identity_transfer line 542
  35. lemma OAI.ContinuousCircleWeight.cappedDiagonal_apply_of_bound line 571
  36. lemma OAI.ContinuousCircleWeight.positive_orbit_capped_pair line 577