OAI/Analysis/LipschitzHilbert/Estimates/FiniteCommutatorSquare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform signed-multiplier commutator bounds imply square-function control. This is the finite randomization step in frequency reassembly.

  1. def OAI.LipschitzHilbert.finiteSignedOperator line 14
  2. theorem OAI.LipschitzHilbert.finiteSignedOperator_apply line 17
  3. theorem OAI.LipschitzHilbert.signed_commutator_apply line 25
  4. theorem OAI.LipschitzHilbert.finite_commutator_square_bound line 35
  5. theorem OAI.LipschitzHilbert.finite_reassembly_square_bound line 45