OAI/NumberTheory/Ostmann/Characters/CharacterAnchorDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The code-preserving diagonal for the constructed character cells

The energy length is the actual bulk density times L. This retains a bulk mass of a L rather than assuming the stronger, generally false, bound L.

  1. theorem OAI.Ostmann.le_characterRangeError line 19
  2. theorem OAI.Ostmann.eventual_character_anchor_decay line 26