OAI/NumberTheory/TwoPoint/Bounds/ActiveStateExpansion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact active-prime states give small scalar expansions after the degree truncation. All absent prime tests remain in each conjunction.

  1. def OAI.TwoPointCorrelations.activeState line 15
  2. def OAI.TwoPointCorrelations.boundedActiveStates line 18
  3. lemma OAI.TwoPointCorrelations.mem_boundedActiveStates line 21
  4. lemma OAI.TwoPointCorrelations.boundedActiveStates_card line 25
  5. def OAI.TwoPointCorrelations.activeStateCircuit line 51
  6. lemma OAI.TwoPointCorrelations.activeStateCircuit_eval line 54
  7. lemma OAI.TwoPointCorrelations.activeStateCircuit_depth line 70
  8. lemma OAI.TwoPointCorrelations.activeStateCircuit_size line 74
  9. theorem OAI.TwoPointCorrelations.activeState_scalar_expansion line 78
  10. lemma OAI.TwoPointCorrelations.activeState_coefficient_mass line 101
  11. theorem OAI.TwoPointCorrelations.activeState_average_comparison line 112