OAI/Combinatorics/BalancedRyser/Profiles/ProfileGridMeasures.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ProfileParameterGrids.rightGridMeasure line 10
  2. instance OAI.Balanced.ProfileParameterGrids.rightGrid_probability line 14
  3. def OAI.Balanced.ProfileParameterGrids.rightGrid line 21
  4. def OAI.Balanced.ProfileParameterGrids.unitUniform line 24
  5. theorem OAI.Balanced.ProfileParameterGrids.integral_rightGrid line 27
  6. theorem OAI.Balanced.ProfileParameterGrids.integral_unitUniform line 35
  7. theorem OAI.Balanced.ProfileParameterGrids.tendsto_rightGrid line 40
  8. def OAI.Balanced.ProfileParameterGrids.powerGrid line 48
  9. def OAI.Balanced.ProfileParameterGrids.powerUniform line 53
  10. theorem OAI.Balanced.ProfileParameterGrids.integral_powerGrid line 58
  11. theorem OAI.Balanced.ProfileParameterGrids.tendsto_powerGrid line 68
  12. theorem OAI.Balanced.ProfileParameterGrids.integral_powerUniform line 74
  13. theorem OAI.Balanced.ProfileParameterGrids.tendsto_rightGrid_prod line 89
  14. theorem OAI.Balanced.ProfileParameterGrids.tendsto_powerGrid_prod line 95
  15. theorem OAI.Balanced.ProfileParameterGrids.rightGrid_prod_open_liminf line 103
  16. theorem OAI.Balanced.ProfileParameterGrids.powerGrid_prod_open_liminf line 110