OAI/Combinatorics/Progressions/Geometry/ProductEquivTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productCoordinate_indicator line 16
  2. theorem OAI.Erdos3.productMean_coordinate_transport line 29
  3. theorem OAI.Erdos3.productCoordinateMix_map line 56
  4. theorem OAI.Erdos3.productConditionalMean_coordinate_transport line 62
  5. theorem OAI.Erdos3.productANOVA_coordinate_transport line 72
  6. theorem OAI.Erdos3.productANOVATruncation_coordinate_transport line 94
  7. theorem OAI.Erdos3.productANOVAEnergy_coordinate_transport line 101
  8. theorem OAI.Erdos3.productSectionAverage_coordinate_transport line 111
  9. theorem OAI.Erdos3.productWeight_coordinate_equiv line 121
  10. theorem OAI.Erdos3.observedProductDensity_coordinate_equiv line 127
  11. theorem OAI.Erdos3.observedProductDensity_coordinate_energy line 137
  12. theorem OAI.Erdos3.productMarginalsClose_coordinate_equiv_iff line 148