OAI/Probability/GaussianReplacement/MixedGeometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.AmbientGrowth line 15
  2. lemma OAI.CurrentProjection.infDist_eq_norm_sub_projection line 19
  3. lemma OAI.CurrentProjection.infDist_submodule_smul line 26
  4. theorem OAI.CurrentProjection.exists_radial_tube_cover line 31
  5. theorem OAI.CurrentProjection.AmbientGrowth.radial_tube line 67
  6. lemma OAI.CurrentProjection.tube_radius_margin line 99
  7. lemma OAI.CurrentProjection.AmbientGrowth.radial_tube_pow line 114
  8. def OAI.CurrentProjection.radialShell line 125
  9. lemma OAI.CurrentProjection.measurableSet_radialShell line 129
  10. theorem OAI.CurrentProjection.AmbientGrowth.shell_normalized_inverse line 134
  11. def OAI.CurrentProjection.mixedInverse line 173
  12. lemma OAI.CurrentProjection.measurable_mixedInverse line 177
  13. def OAI.CurrentProjection.shellConstant line 184
  14. lemma OAI.CurrentProjection.inverse_div_factor line 186
  15. lemma OAI.CurrentProjection.radial_power_cancel line 191
  16. theorem OAI.CurrentProjection.AmbientGrowth.shell_mixed_inverse line 198
  17. lemma OAI.CurrentProjection.dyadic_min_sum_le line 251
  18. lemma OAI.CurrentProjection.shellConstant_nonneg line 315
  19. lemma OAI.CurrentProjection.shellConstant_mono line 319
  20. lemma OAI.CurrentProjection.mem_radialShell_dyadic line 330
  21. theorem OAI.CurrentProjection.AmbientGrowth.mixed_inverse_le line 341
  22. lemma OAI.CurrentProjection.two_pow_le_exp line 417
  23. lemma OAI.CurrentProjection.shellConstant_exp_bound line 423
  24. def OAI.CurrentProjection.sphereLift line 442
  25. lemma OAI.CurrentProjection.LocalGrowth.sphereLift line 445
  26. lemma OAI.CurrentProjection.sphereLift_ae_norm_sub_le line 451
  27. theorem OAI.CurrentProjection.localGrowth_mixed_inverse line 462