OAI/NumberTheory/TwoPoint/Bounds/PaddingStateWeights.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual retained departure coefficient is an explicit function of the finite padding states at its two endpoints. This is the scalar coefficient used in the signed finite-law expansion.

  1. def OAI.TwoPointCorrelations.paddingStateDensity line 15
  2. def OAI.TwoPointCorrelations.paddingStateKeep line 20
  3. def OAI.TwoPointCorrelations.paddingStateDeparture line 24
  4. lemma OAI.TwoPointCorrelations.paddingDensity_eq_state line 33
  5. lemma OAI.TwoPointCorrelations.integerEdgeKeep_eq_state line 45
  6. lemma OAI.TwoPointCorrelations.retainedEdgeDeparture_eq_state line 54
  7. lemma OAI.TwoPointCorrelations.paddingStateDeparture_nonneg line 69
  8. lemma OAI.TwoPointCorrelations.paddingStateDeparture_le line 78