OAI/Combinatorics/Progressions/Estimates/AnchoredReferenceDomination.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.expect_subset_le_card_ratio line 13
  2. theorem OAI.Erdos3.expect_injective_le_card_ratio line 24
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_finset_expect line 35
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.translated_subset_mixture_le line 42
  5. theorem OAI.Erdos3.abs_expect_parent_sub_subset_le_Icc line 66
  6. theorem OAI.Erdos3.abs_expect_parent_sub_subset_le_unit line 102
  7. theorem OAI.Erdos3.abs_expect_parent_sub_subset_le_abs line 109
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_above_double_cap_le line 129
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_above_double_cap_le_of_excess line 147
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.siteLaw_excess_le line 162
  11. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_physical_event_le line 201
  12. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_physical_excess_le line 211
  13. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_physical_tail_le line 224
  14. theorem OAI.Erdos3.normalizedEarlyFiberCap_exp_bound line 239
  15. theorem OAI.Erdos3.trimmedIntegerBox_card_ratio_le_two line 264
  16. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_trimmed_reference_le line 283
  17. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_trimmed_domination_transfer line 312
  18. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_anchored_trimmed_reference_le line 343
  19. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_anchored_trimmed_domination_transfer line 372