OAI/Probability/GaussianReplacement/FiberGeometry.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.directionComplement line 18
  2. lemma OAI.CurrentProjection.directionComplement_apply line 22
  3. lemma OAI.CurrentProjection.directionComplement_inner line 25
  4. lemma OAI.CurrentProjection.gaussian_direction_indep line 31
  5. lemma OAI.CurrentProjection.gaussian_direction_real line 48
  6. lemma OAI.CurrentProjection.gaussian_direction_split line 59
  7. lemma OAI.CurrentProjection.gaussian_direction_rows_split line 71
  8. lemma OAI.CurrentProjection.gaussian_direction_rows_recover line 86
  9. lemma OAI.CurrentProjection.tendsto_normalized_closedBall line 105
  10. lemma OAI.CurrentProjection.ennreal_double_mul_le_sq_add line 147
  11. lemma OAI.CurrentProjection.cube_energy_contraction line 158
  12. lemma OAI.CurrentProjection.continuous_lintegral_bounded line 193
  13. lemma OAI.CurrentProjection.tendsto_scaled_cube_average line 205
  14. def OAI.CurrentProjection.gaussianReconstruct line 247
  15. lemma OAI.CurrentProjection.gaussian_reconstruct_law line 250
  16. lemma OAI.CurrentProjection.gaussian_reconstruct_pairing line 271
  17. lemma OAI.CurrentProjection.continuous_gaussian_slice line 277
  18. def OAI.CurrentProjection.fiberEnergyBound line 294
  19. lemma OAI.CurrentProjection.fiberEnergyBound_ne_top line 296
  20. lemma OAI.CurrentProjection.uniformSphere_ae_ne line 298
  21. lemma OAI.CurrentProjection.spherical_inverse_bound line 307
  22. lemma OAI.CurrentProjection.spherical_cube_expectation line 321
  23. lemma OAI.CurrentProjection.spherical_extended_energy line 340
  24. lemma OAI.CurrentProjection.spherical_projection_ac line 361
  25. lemma OAI.CurrentProjection.projection_convolution_contraction line 372
  26. lemma OAI.CurrentProjection.cubeVectorKernel_normalized line 393
  27. lemma OAI.CurrentProjection.cubeAverage_labelKernel line 398
  28. lemma OAI.CurrentProjection.spherical_cube_energy_eq line 409
  29. lemma OAI.CurrentProjection.lintegral_labelLaw line 427
  30. lemma OAI.CurrentProjection.spherical_cube_energy_le line 432
  31. lemma OAI.CurrentProjection.spherical_quadratic_limit line 450