OAI/Analysis/FiniteFactor/Coupling/Bounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.CouplingParameters.minimumLength line 11
2. theorem OAI.FiniteFactor.CouplingParameters.minimumLength_pos line 14
3. theorem OAI.FiniteFactor.CouplingParameters.minimumLength_le line 19
4. theorem OAI.FiniteFactor.CouplingParameters.weighted_minimumLength_le line 26
5. theorem OAI.FiniteFactor.CouplingParameters.weighted_inverse_length_le line 38
6. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_upper line 46
7. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_lt_ten line 59
8. theorem OAI.FiniteFactor.CouplingParameters.weighted_minimumLength_energy line 63
9. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_energy line 74
10. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_source_energy line 101