OAI/Combinatorics/Progressions/Estimates/RelativePatchAmplification.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.relativePatchComplexity line 15
  2. def OAI.Erdos3.relativePatchDistinctWeights line 19
  3. def OAI.Erdos3.relativePatchBoxScore line 23
  4. def OAI.Erdos3.relativePatchSliceScore line 28
  5. def OAI.Erdos3.RelativePatchSliceConclusion line 34
  6. def OAI.Erdos3.RelativePatchAbsoluteRule line 42
  7. def OAI.Erdos3.RelativePatchInductionRule line 53
  8. def OAI.Erdos3.RelativePatchPowerInductionRule line 69
  9. theorem OAI.Erdos3.relativePatchComplexity_rank_le line 72
  10. theorem OAI.Erdos3.relativePatchDistinctWeights_eq_zero_iff line 78
  11. theorem OAI.Erdos3.RelativePatchSliceConclusion.mono line 91
  12. theorem OAI.Erdos3.RelativePatchInductionRule.mono line 103
  13. theorem OAI.Erdos3.recursive_discount_target_mem_Icc line 123
  14. theorem OAI.Erdos3.RelativePatchSliceConclusion.cost_nonneg line 132
  15. theorem OAI.Erdos3.frozen_side_le_exp_of_keep_threshold line 138
  16. theorem OAI.Erdos3.RelativePatchAbsoluteRule.mono line 154
  17. theorem OAI.Erdos3.exists_relativePatch_finite_stage_power_assembly line 169
  18. theorem OAI.Erdos3.exists_relativePatch_majorized_stage_power_assembly line 196
  19. theorem OAI.Erdos3.relativePatchComplexity_kernel_bound line 231
  20. theorem OAI.Erdos3.log_length_lower_of_exp_slice line 243
  21. theorem OAI.Erdos3.relativePatchBoxScore_rank_zero line 263
  22. theorem OAI.Erdos3.relativePatch_mean_increment_of_zero_weights line 269
  23. theorem OAI.Erdos3.relativePatch_density_increment_of_zero_weights line 284
  24. def OAI.Erdos3.ResidueBoxSlice.identity line 307
  25. def OAI.Erdos3.ResidueBoxSlice.comp line 312
  26. theorem OAI.Erdos3.ResidueBoxSlice.comp_point line 320
  27. def OAI.Erdos3.ResidueBoxSlice.polynomial line 326
  28. theorem OAI.Erdos3.ResidueBoxSlice.polynomial_degree line 329
  29. theorem OAI.Erdos3.ResidueBoxSlice.polynomial_eval line 338
  30. theorem OAI.Erdos3.VectorPolynomial.coefficients_substitute_mem line 348
  31. theorem OAI.Erdos3.VectorPolynomial.eval_slice_substitute line 356
  32. theorem OAI.Erdos3.ResidueBoxSlice.comp_length_exp_lower line 374
  33. def OAI.Erdos3.ResidueBoxSlice.integerAffine line 404
  34. def OAI.Erdos3.ResidueBoxSlice.integerPullback line 407
  35. theorem OAI.Erdos3.ResidueBoxSlice.integerAffine_finPoint line 410
  36. theorem OAI.Erdos3.ResidueBoxSlice.integerAffine_mem_integerBox line 417
  37. theorem OAI.Erdos3.ResidueBoxSlice.pullback_mem_Icc line 433
  38. theorem OAI.Erdos3.ResidueBoxSlice.pullback_apFree line 440
  39. theorem OAI.Erdos3.ResidueBoxSlice.integerAffine_comp line 464
  40. theorem OAI.Erdos3.ResidueBoxSlice.integerPullback_comp line 471
  41. theorem OAI.Erdos3.relativePatchBoxScore_pullback line 479
  42. theorem OAI.Erdos3.relativePatchSliceScore_comp line 504
  43. theorem OAI.Erdos3.RelativePatchSliceConclusion.comp line 516
  44. theorem OAI.Erdos3.relativePatchDistinctWeights_le_degree line 540
  45. def OAI.Erdos3.LowDensityRelativeAbsoluteRule line 549
  46. theorem OAI.Erdos3.RelativePatchPowerInductionRule.amplify line 553
  47. theorem OAI.Erdos3.LowDensityRelativeAbsoluteRule.amplify line 593
  48. theorem OAI.Erdos3.LowDensityRelativeAbsoluteRule.amplify_power line 609