OAI/GroupTheory/SimpleAmenable/RandomFields/HellingerDistance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.integral_abs_mul_le_sqrt line 15
  2. theorem OAI.SimpleAmenable.density_L1_le_twice_root_distance line 26
  3. theorem OAI.SimpleAmenable.affineNoiseRoot_memLp line 57
  4. theorem OAI.SimpleAmenable.affineNoiseRoot_square_distance line 64
  5. theorem OAI.SimpleAmenable.affineNoiseDensity_L1_distance line 89
  6. theorem OAI.SimpleAmenable.measurableEquiv_map_withDensity line 110
  7. theorem OAI.SimpleAmenable.smoothNoiseLaw_pi_density line 119
  8. theorem OAI.SimpleAmenable.independentSmoothNoiseLaw_finite_density line 150
  9. def OAI.SimpleAmenable.finiteAffineNoiseLaw line 155
  10. instance OAI.SimpleAmenable.finiteAffineNoiseLaw_probability line 159
  11. theorem OAI.SimpleAmenable.finiteAffineNoiseLaw_density line 164