OAI/Combinatorics/Progressions/Estimates/NormalizedTwistCellSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FiniteProbabilityWeights.fiberComplexMean line 11
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.sum_fiberComplexMean_on line 15
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_mul_condition_complexMean line 25
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberComplexMean_eq_condition line 32
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.sum_condition_complexMean_on line 41
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.retained_condition_mixture_error line 56
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.sum_fiber_masses_le_one line 68
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_condition_embedding_complexMean line 89
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_embedded_fiber_complexMean line 111
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_large_correlating_fiber line 141
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_large_correlating_fiber_of_approximation line 188