OAI/Analysis/IrrationalRotation/Sampling/UniformIntervalPhase.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.UniformIntervalPhase.map_interval_nat line 13
  2. theorem OAI.Invariant233.UniformIntervalPhase.map_interval_le_haar line 30
  3. theorem OAI.Invariant233.UniformIntervalPhase.map_interval_sandwich line 39
  4. theorem OAI.Invariant233.UniformIntervalPhase.rnDeriv_le_const_of_le_smul line 60
  5. theorem OAI.Invariant233.UniformIntervalPhase.const_le_rnDeriv_of_smul_le line 71
  6. theorem OAI.Invariant233.UniformIntervalPhase.phaseLaw_sandwich line 83
  7. theorem OAI.Invariant233.UniformIntervalPhase.real_density_spec_of_sandwich line 110
  8. theorem OAI.Invariant233.UniformIntervalPhase.phaseDensity_spec line 151
  9. theorem OAI.Invariant233.UniformIntervalPhase.intervalLaw_map_mul line 160
  10. theorem OAI.Invariant233.UniformIntervalPhase.sampled_phaseLaw line 177
  11. theorem OAI.Invariant233.UniformIntervalPhase.lambdaLaw_eq_intervalLaw line 186
  12. theorem OAI.Invariant233.UniformIntervalPhase.scalar_marginal_circle line 192
  13. theorem OAI.Invariant233.UniformIntervalPhase.measurable_representative line 204
  14. theorem OAI.Invariant233.UniformIntervalPhase.representative_coe line 207
  15. theorem OAI.Invariant233.UniformIntervalPhase.map_representative_haar line 211
  16. theorem OAI.Invariant233.UniformIntervalPhase.fractionLaw_eq_map_phaseLaw line 227
  17. theorem OAI.Invariant233.UniformIntervalPhase.scalar_marginal line 234
  18. theorem OAI.Invariant233.UniformIntervalPhase.lambdaLaw_probability line 251
  19. theorem OAI.Invariant233.UniformIntervalPhase.fractionDensity_le_two line 261
  20. theorem OAI.Invariant233.UniformIntervalPhase.lambdaLaw_eq_cond line 269
  21. theorem OAI.Invariant233.UniformIntervalPhase.sampled_circle_le_two line 275
  22. theorem OAI.Invariant233.UniformIntervalPhase.integral_sample_le_two line 293
  23. theorem OAI.Invariant233.UniformIntervalPhase.norm_integral_phase_sub_le line 309
  24. theorem OAI.Invariant233.UniformIntervalPhase.norm_integral_sample_sub_le line 346