OAI/NumberTheory/CubicMoment/Decomposition/StoppedOverlapScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative overlap saving with the genuine active roughness threshold. The outer energy and inner bounded coefficient have separate constants.

  1. theorem OAI.CubicFirstMoment.bounded_active_model_overlap_log_saving line 11