OAI/Combinatorics/Progressions/Probability/CylinderJointMass.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.FiniteProbabilityCoupling line 14
  2. def OAI.Erdos3.FiniteProbabilityCoupling.ofKernel line 20
  3. def OAI.Erdos3.productCouplingPairing line 34
  4. theorem OAI.Erdos3.productCoupling_left_mean line 38
  5. theorem OAI.Erdos3.productCoupling_right_mean line 43
  6. theorem OAI.Erdos3.productCouplingPairing_sq_le line 48
  7. theorem OAI.Erdos3.productCouplingPairing_ANOVA_ne line 58
  8. theorem OAI.Erdos3.productCouplingPairing_truncation line 66
  9. theorem OAI.Erdos3.productCouplingPairing_truncation_sq_le line 79
  10. theorem OAI.Erdos3.ProductDependsOn.coordinateMap line 96
  11. theorem OAI.Erdos3.productCouplingPairing_blocks line 107
  12. theorem OAI.Erdos3.productCouplingPairing_ANOVA_blocks line 129
  13. theorem OAI.Erdos3.productCouplingPairing_complete_inside line 160
  14. def OAI.Erdos3.productCouplingAtomMass line 192
  15. theorem OAI.Erdos3.productCouplingPairing_indicators line 195
  16. theorem OAI.Erdos3.productCouplingAtomMass_nonneg line 209
  17. theorem OAI.Erdos3.productCouplingAtomMass_le_one line 213
  18. theorem OAI.Erdos3.productCouplingPairing_complete_atom line 221
  19. theorem OAI.Erdos3.productCouplingPairing_sum_left line 250
  20. theorem OAI.Erdos3.productCouplingPairing_sum_right line 256
  21. theorem OAI.Erdos3.productCouplingAtomMass_sum_right line 262
  22. theorem OAI.Erdos3.productCouplingAtomMass_sum_left line 272
  23. theorem OAI.Erdos3.productCouplingAtomMass_sum line 282
  24. theorem OAI.Erdos3.productCouplingPairing_atom_partition line 288
  25. theorem OAI.Erdos3.productCouplingAtomMass_weighted_error line 300
  26. def OAI.Erdos3.ProductCylinder.referenceMass line 327
  27. theorem OAI.Erdos3.ProductCylinder.referenceMass_mul_mass line 331
  28. theorem OAI.Erdos3.ProductCylinder.referenceMass_mul_cut_mass line 349
  29. theorem OAI.Erdos3.CylinderRemovalChain.reference_mass_sum line 357
  30. theorem OAI.Erdos3.CylinderRemovalChain.reference_mass_sum_le_one line 380
  31. theorem OAI.Erdos3.CylinderRemovalChain.joint_mass_sum line 409
  32. theorem OAI.Erdos3.CylinderRemovalChain.joint_mass_sum_le_one line 421