OAI/Analysis/IrrationalRotation/Couplings/CouplingMarginalBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.CouplingMarginalBounds.rho_nonneg line 11
  2. lemma OAI.Invariant233.CouplingMarginalBounds.width_pos line 14
  3. lemma OAI.Invariant233.CouplingMarginalBounds.sqrt_width_div_le line 17
  4. lemma OAI.Invariant233.CouplingMarginalBounds.rho_le_mul_width line 26
  5. lemma OAI.Invariant233.CouplingMarginalBounds.rho_div_width_le line 30
  6. lemma OAI.Invariant233.CouplingMarginalBounds.rho_sq_div_width line 34
  7. lemma OAI.Invariant233.CouplingMarginalBounds.diagonalMass_bounds line 40
  8. lemma OAI.Invariant233.CouplingMarginalBounds.marginal_density_bounds line 60
  9. lemma OAI.Invariant233.CouplingMarginalBounds.ae_eq_of_ordered_equal_integral line 116
  10. lemma OAI.Invariant233.CouplingMarginalBounds.ae_eq_of_coordinate_ordered_equal_integral line 123
  11. lemma OAI.Invariant233.CouplingMarginalBounds.integral_sq_sum_le line 134
  12. lemma OAI.Invariant233.CouplingMarginalBounds.integral_sq_weighted_sum_le line 154
  13. lemma OAI.Invariant233.CouplingMarginalBounds.uniformDensity_memLp line 162
  14. lemma OAI.Invariant233.CouplingMarginalBounds.uniformDensity_integral line 167
  15. lemma OAI.Invariant233.CouplingMarginalBounds.uniformDensity_sq_integral line 173
  16. lemma OAI.Invariant233.CouplingMarginalBounds.uniformDensity_variance line 183
  17. lemma OAI.Invariant233.CouplingMarginalBounds.uniformDensity_variance_le line 201
  18. lemma OAI.Invariant233.CouplingMarginalBounds.diagonalMass_add_components line 213
  19. lemma OAI.Invariant233.CouplingMarginalBounds.conditional_component_lower line 219
  20. lemma OAI.Invariant233.CouplingMarginalBounds.five_component_energy_bound line 227