OAI/Analysis/IrrationalRotation/Couplings/ConditionalConvolution.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InvariantProjection.ConditionalConvolution.exceptionalTail line 19
  2. theorem OAI.InvariantProjection.ConditionalConvolution.exceptionalTail_nonneg line 25
  3. theorem OAI.InvariantProjection.ConditionalConvolution.exceptionalTail_eq_productMask line 33
  4. theorem OAI.InvariantProjection.ConditionalConvolution.exceptionalTail_eq_indicatorOne line 45
  5. theorem OAI.InvariantProjection.ConditionalConvolution.Data.coeffA_measurable line 59
  6. theorem OAI.InvariantProjection.ConditionalConvolution.Data.coeffB_measurable line 65
  7. theorem OAI.InvariantProjection.ConditionalConvolution.Data.integrableOn_norm_truncated line 72
  8. theorem OAI.InvariantProjection.ConditionalConvolution.Data.first_tail_bound line 80
  9. theorem OAI.InvariantProjection.ConditionalConvolution.Data.second_tail_bound line 92
  10. theorem OAI.InvariantProjection.ConditionalConvolution.Data.integral_truncated_le_of_pointwise line 104
  11. theorem OAI.InvariantProjection.ConditionalConvolution.Data.pointwise_truncated_bound line 145
  12. theorem OAI.InvariantProjection.ConditionalConvolution.Data.obstruction_of_pointwise line 160
  13. theorem OAI.InvariantProjection.ConditionalConvolution.conditional_convolution_obstruction line 186