OAI/Analysis/FiniteFactor/Coupling/Mixture.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.mixtureDensity line 14
  2. theorem OAI.FiniteFactor.mixtureDensity_memLp line 17
  3. theorem OAI.FiniteFactor.mixtureDensity_integral line 21
  4. theorem OAI.FiniteFactor.mixtureDensity_energy_le line 31
  5. def OAI.FiniteFactor.unitIntervalMeasure line 63

    Also declared: ComparatorChallenges/ProductBrown.lean:125 (same declaration text).

  6. instance OAI.FiniteFactor.(instance at line 65) line 65
  7. theorem OAI.FiniteFactor.unitIntervalMeasure_interval line 69
  8. def OAI.FiniteFactor.CouplingParameters.endpointLength line 77
  9. def OAI.FiniteFactor.CouplingParameters.endpointInterval line 80
  10. def OAI.FiniteFactor.CouplingParameters.endpointComponentDensity line 83
  11. def OAI.FiniteFactor.CouplingParameters.endpointDensity line 86
  12. theorem OAI.FiniteFactor.CouplingParameters.endpointLength_pos line 89
  13. theorem OAI.FiniteFactor.CouplingParameters.endpointLength_le line 92
  14. theorem OAI.FiniteFactor.CouplingParameters.endpointInterval_measurable line 98
  15. theorem OAI.FiniteFactor.CouplingParameters.endpointInterval_mass line 102
  16. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_memLp line 114
  17. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_integral line 119
  18. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_lower line 129