OAI/Analysis/FiniteFactor/Coupling/Parameters.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.FiniteFactor.CouplingParameters line 16

    Source documentation

    One block of the actual coupling, with two distinct width labels. The boolean records whether this is the tagged block.

    structure CouplingParameters where
…
  2. theorem OAI.FiniteFactor.CouplingParameters.m_pos line 30
  3. theorem OAI.FiniteFactor.CouplingParameters.width_pos line 31
  4. def OAI.FiniteFactor.CouplingParameters.rho line 34
  5. def OAI.FiniteFactor.CouplingParameters.tagMass line 35
  6. def OAI.FiniteFactor.CouplingParameters.diagonalMass line 36
  7. theorem OAI.FiniteFactor.CouplingParameters.rho_nonneg line 38
  8. theorem OAI.FiniteFactor.CouplingParameters.rho_le line 41
  9. theorem OAI.FiniteFactor.CouplingParameters.rho_div_width_le line 49
  10. theorem OAI.FiniteFactor.CouplingParameters.rho_energy line 52
  11. theorem OAI.FiniteFactor.CouplingParameters.tagMass_nonneg line 56
  12. theorem OAI.FiniteFactor.CouplingParameters.tagMass_le line 62
  13. theorem OAI.FiniteFactor.CouplingParameters.diagonalMass_lower line 68
  14. theorem OAI.FiniteFactor.CouplingParameters.diagonalMass_pos line 74
  15. theorem OAI.FiniteFactor.CouplingParameters.diagonalMass_le line 76
  16. def OAI.FiniteFactor.CouplingParameters.replacementMass line 82

    Source documentation

    0/1 are top/bottom of width 0, 2/3 of width 1, 4 is the tag. In particular equal numerical widths do not identify labels.

    def replacementMass : Fin 5 → ℝ :=
…
  17. def OAI.FiniteFactor.CouplingParameters.leftLength line 85
  18. def OAI.FiniteFactor.CouplingParameters.rightLength line 88
  19. theorem OAI.FiniteFactor.CouplingParameters.replacementMass_nonneg line 91
  20. theorem OAI.FiniteFactor.CouplingParameters.mass_sum line 94
  21. theorem OAI.FiniteFactor.CouplingParameters.leftLength_pos line 98
  22. theorem OAI.FiniteFactor.CouplingParameters.rightLength_pos line 106
  23. theorem OAI.FiniteFactor.CouplingParameters.lengths_sum_le line 114