OAI/NumberTheory/CubicMoment/Decomposition/StoppingBoundaryShift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An active logarithmic boundary for a larger ambient envelope, with roughness still measured in the original parameter X. The index shift is chosen explicitly, so no comparison of logarithms of two scales is needed.

  1. lemma OAI.CubicFirstMoment.geometric_boundary_shift line 13
  2. theorem OAI.CubicFirstMoment.eventually_stopping_active_boundary_envelope line 21