OAI/Combinatorics/Progressions/Estimates/ComplexSampledSquarePerturbation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.complex_model_l1_le_of_bounded_tests line 12

    Also declared: OAI/Combinatorics/Progressions/Estimates/ComplexModelComparisonL1.lean:12 (same declaration text).

  2. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_integral line 41

    Also declared: OAI/Combinatorics/Progressions/Estimates/ComplexModelComparisonL1.lean:42 (same declaration text).

  3. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_density_test_integral line 50

    Also declared: OAI/Combinatorics/Progressions/Estimates/ComplexModelComparisonL1.lean:51 (same declaration text).

  4. theorem OAI.Erdos3.complex_model_l2_le_of_l1 line 72
  5. theorem OAI.Erdos3.complex_norm_sub_sq_le line 105
  6. theorem OAI.Erdos3.complex_square_integral_uniform_perturbation line 112
  7. theorem OAI.Erdos3.finiteComplex_norm_sq_expansion line 147
  8. theorem OAI.Erdos3.finiteComplex_quadratic_error_le line 161
  9. theorem OAI.Erdos3.finiteComplex_norm_sq_integral line 179
  10. theorem OAI.Erdos3.finiteComplex_l2_integral_comparison line 192
  11. theorem OAI.Erdos3.complex_square_sub_integrable line 217
  12. theorem OAI.Erdos3.complex_sampled_square_perturbation line 230