OAI/Analysis/LipschitzHilbert/Estimates/ProductPerturbation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Accumulating pointwise prediction errors without a loss per level.

  1. theorem OAI.LipschitzHilbert.product_le_exp_sum line 18
  2. theorem OAI.LipschitzHilbert.product_le_of_error_budget line 27
  3. theorem OAI.LipschitzHilbert.integrable_perturbed_product line 35
  4. theorem OAI.LipschitzHilbert.integral_perturbed_product_le line 50