OAI/Combinatorics/Progressions/Estimates/RelativePatchPositivePowerInduction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerBox_real_expect_eq_residue line 14
  2. theorem OAI.Erdos3.relativePatchSliceScore_identity line 39
  3. theorem OAI.Erdos3.exists_initial_relative_absolute_rule line 62
  4. theorem OAI.Erdos3.ResidueBoxSlice.polynomial_weighted_support line 136
  5. theorem OAI.Erdos3.PolynomialPatch.LowestLayerModel.normalizedOrigin_vector_degree line 152
  6. theorem OAI.Erdos3.PolynomialPatch.LowestLayerModel.exists_actual_prepared_slice line 160
  7. theorem OAI.Erdos3.BooleanCubeKernel.unconditionedAbsoluteSample_input line 258
  8. theorem OAI.Erdos3.PolynomialPatch.LowestLayerModel.exists_uniform_prepared_slice line 312
  9. theorem OAI.Erdos3.BooleanCubeKernel.smoothAffineSample_jointIntegerFrame line 375
  10. theorem OAI.Erdos3.BooleanCubeKernel.smoothAffineSample_inside_of_residue_sites line 384
  11. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_arbitrary_absolute_family line 413
  12. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_arbitrary_absolute_family_of_zero_score line 468
  13. theorem OAI.Erdos3.exists_lowest_weight_prepared_patch line 521
  14. theorem OAI.Erdos3.exists_lowest_weight_early_late_preparation line 600
  15. def OAI.Erdos3.PreparedRelativePatchPowerPassage line 723
  16. def OAI.Erdos3.RelativePatchFinPositivePowerRule line 757
  17. theorem OAI.Erdos3.exists_relativePatchFinPositivePower_of_prepared line 772
  18. def OAI.Erdos3.RelativePatchFinPowerInductionRule line 837
  19. theorem OAI.Erdos3.RelativePatchFinPowerInductionRule.to_general line 842
  20. theorem OAI.Erdos3.RelativePatchPowerInductionRule.to_fin line 848
  21. theorem OAI.Erdos3.RelativePatchFinPowerInductionRule.mono line 854
  22. theorem OAI.Erdos3.relativePatchFinPowerInductionRule_of_zero_and_positive line 866
  23. theorem OAI.Erdos3.exists_relativePatchFinPowerInductionRule_of_positive_successors line 894
  24. theorem OAI.Erdos3.exists_relativePatchPowerInductionRule_of_fin_base_positive_successors line 922
  25. theorem OAI.Erdos3.exists_relativePatchPowerInductionRule_of_positive_successors line 939