OAI/Analysis/LipschitzHilbert/Trees/SourceCappedStepArithmetic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Normalize removal budgets while keeping the independent size cap.

  1. theorem OAI.LipschitzHilbert.combine_capped_removal_budgets line 10
  2. theorem OAI.LipschitzHilbert.min_scaled_le line 30
  3. theorem OAI.LipschitzHilbert.capped_density_weight_le line 38
  4. theorem OAI.LipschitzHilbert.modelSizeThreshold_eq_sqrt_ratio line 51