OAI/Analysis/RotationWeights/PhaseWeights.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CircleSampling.CircleX line 33
  2. instance OAI.CircleSampling.(instance at line 35) line 35
  3. lemma OAI.CircleSampling.volume_singleton_zero line 40
  4. def OAI.CircleSampling.repr line 44
  5. lemma OAI.CircleSampling.measurable_repr line 45
  6. lemma OAI.CircleSampling.repr_mem line 47
  7. lemma OAI.CircleSampling.repr_coe line 49
  8. lemma OAI.CircleSampling.coe_repr line 51
  9. lemma OAI.CircleSampling.integral_repr line 54
  10. def OAI.CircleSampling.delta line 63
  11. def OAI.CircleSampling.weight line 64
  12. def OAI.CircleSampling.uPos line 66
  13. def OAI.CircleSampling.uNeg line 67
  14. lemma OAI.CircleSampling.measurable_delta line 69
  15. lemma OAI.CircleSampling.measurable_weight line 70
  16. lemma OAI.CircleSampling.measurable_uPos line 76
  17. lemma OAI.CircleSampling.measurable_uNeg line 79
  18. lemma OAI.CircleSampling.weight_bounds line 82
  19. lemma OAI.CircleSampling.delta_lipschitz line 91
  20. lemma OAI.CircleSampling.delta_pos line 98
  21. lemma OAI.CircleSampling.delta_le_half line 100
  22. lemma OAI.CircleSampling.weight_integral_t line 106
  23. lemma OAI.CircleSampling.uPos_integral_t line 128
  24. lemma OAI.CircleSampling.integral_uPos line 134
  25. lemma OAI.CircleSampling.integrable_uPos line 152
  26. lemma OAI.CircleSampling.integrable_uNeg line 159
  27. lemma OAI.CircleSampling.integral_uNeg line 166
  28. lemma OAI.CircleSampling.weight_sq_integral_t line 176
  29. lemma OAI.CircleSampling.integral_inv_delta line 187
  30. lemma OAI.CircleSampling.integral_uPos_sq line 226
  31. lemma OAI.CircleSampling.integral_uNeg_sq line 245
  32. lemma OAI.CircleSampling.uNeg_unwrapped line 266
  33. lemma OAI.CircleSampling.uNeg_integral_real line 291
  34. lemma OAI.CircleSampling.negative_weight_upper line 302
  35. lemma OAI.CircleSampling.negative_weight_lower line 322
  36. lemma OAI.CircleSampling.integrable_negative_weight line 341
  37. lemma OAI.CircleSampling.negative_density_upper line 350
  38. lemma OAI.CircleSampling.negative_density_lower line 373
  39. lemma OAI.CircleSampling.integral_delta_small line 396
  40. lemma OAI.CircleSampling.uNeg_mean_bounds line 424
  41. lemma OAI.CircleSampling.integral_uNeg_mean_sq line 439