OAI/NumberTheory/DukePrimeDegree/Dynamics/IntegrableCoboundary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integrable coboundaries have zero mean

Only the difference is assumed integrable. Truncating the transfer function by one-Lipschitz clamps and applying dominated convergence avoids any integrability assumption on the logarithmic normalization.

  1. def OAI.DukePrimeDegree.realClamp line 17
  2. lemma OAI.DukePrimeDegree.realClamp_lipschitz line 19
  3. lemma OAI.DukePrimeDegree.realClamp_eq line 22
  4. lemma OAI.DukePrimeDegree.realClamp_abs_le line 26
  5. lemma OAI.DukePrimeDegree.realClamp_difference_le line 32
  6. theorem OAI.DukePrimeDegree.integral_coboundary_eq_zero line 37