OAI/Probability/RadialTransition/SpatialProducts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.orderedEnergy line 14
  2. theorem OAI.RadialTransition.orderedEnergy_fin line 18
  3. theorem OAI.RadialTransition.orderedEnergy_equiv line 36
  4. theorem OAI.RadialTransition.continuous_orderedEnergy line 49
  5. theorem OAI.RadialTransition.orderedEnergy_abs_bound line 62
  6. theorem OAI.RadialTransition.integrable_orderedBoltzmann line 82
  7. def OAI.RadialTransition.rawPartition line 99
  8. def OAI.RadialTransition.partitionOn line 102
  9. theorem OAI.RadialTransition.rawPartition_nonneg line 105
  10. theorem OAI.RadialTransition.rawPartition_equiv line 108
  11. theorem OAI.RadialTransition.measure_pi_add line 120
  12. theorem OAI.RadialTransition.sum_split_four line 140
  13. theorem OAI.RadialTransition.orderedEnergy_split line 152
  14. theorem OAI.RadialTransition.orderedEnergy_split_le line 188
  15. theorem OAI.RadialTransition.sector_product_integral line 202
  16. theorem OAI.RadialTransition.sector_raw_lower line 218
  17. theorem OAI.RadialTransition.rawPartition_union_sum line 266
  18. theorem OAI.RadialTransition.rawPartition_union_lower line 285
  19. theorem OAI.RadialTransition.partitionOn_union_lower line 322