OAI/Analysis/IrrationalRotation/Couplings/BiasedTailDensity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.BiasedTailDensity.sq_integral_le_integral_sq line 17
  2. theorem OAI.Invariant233.BiasedTailDensity.integrable_tailDensity line 39
  3. theorem OAI.Invariant233.BiasedTailDensity.ae_sq_tailDensity_le line 43
  4. theorem OAI.Invariant233.BiasedTailDensity.memLp_tailDensity line 49
  5. theorem OAI.Invariant233.BiasedTailDensity.integral_sq_tailDensity_le line 60
  6. theorem OAI.Invariant233.BiasedTailDensity.eLpNorm_tailDensity_le line 68
  7. theorem OAI.Invariant233.BiasedTailDensity.integral_tailDensity line 78
  8. theorem OAI.Invariant233.BiasedTailDensity.map_snd_withDensity_lintegral line 82
  9. theorem OAI.Invariant233.BiasedTailDensity.ae_nonneg_tailDensity line 95
  10. theorem OAI.Invariant233.BiasedTailDensity.map_snd_withDensity_tailDensity line 102
  11. theorem OAI.Invariant233.BiasedTailDensity.tailDensity_spec line 114