OAI/Analysis/LipschitzHilbert/Trees/SourceWideLogMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's full disparity window reaches log ratio = 2L. Its polynomial top-count factor therefore needs a third logarithmic unit. The same phase subpower bound survives this extra fixed unit.

  1. theorem OAI.LipschitzHilbert.eventually_count_log_bound_wide line 15
  2. theorem OAI.LipschitzHilbert.source_phase_mass_bound_wide line 36
  3. theorem OAI.LipschitzHilbert.eventually_source_subpower_amplitude_wide line 55
  4. theorem OAI.LipschitzHilbert.eventually_source_amplitude_squared_decay_wide line 98