OAI/Geometry/CubicTorus/Estimates/BVBallProbability.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.lipschitz_affine_line line 15
  2. theorem OAI.CubicTorus.lipschitz_translation_square_le line 23
  3. theorem OAI.CubicTorus.lipschitz_average_translation_square_le line 110
  4. lemma OAI.CubicTorus.probability_dominated_square line 191
  5. theorem OAI.CubicTorus.h1_average_bounds line 209
  6. def OAI.CubicTorus.ballProbability line 276
  7. lemma OAI.CubicTorus.closedBall_haar_ne_zero line 280
  8. lemma OAI.CubicTorus.ballProbability_isProbability line 286
  9. lemma OAI.CubicTorus.ballProbability_domination line 294
  10. lemma OAI.CubicTorus.ballProbability_ae_norm_le line 301
  11. lemma OAI.CubicTorus.ballProbability_density_ne_top line 308
  12. lemma OAI.CubicTorus.boundedContinuous_L2_dist_sq line 324
  13. lemma OAI.CubicTorus.h1_average_error line 342
  14. theorem OAI.CubicTorus.totallyBounded_local_H1 line 362
  15. theorem OAI.CubicTorus.local_H1_subsequence line 460
  16. lemma OAI.CubicTorus.L2_pairing_tendsto line 482
  17. lemma OAI.CubicTorus.L2_pairing_limit_zero line 489
  18. theorem OAI.CubicTorus.restricted_H1_subsequence line 508