OAI/Probability/SKGap/Localization/ResidualInduction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Primary.mag line 15
  2. def OAI.SKGapCutoff.Primary.fld line 18
  3. def OAI.SKGapCutoff.Primary.onsager line 21
  4. def OAI.SKGapCutoff.Primary.residual line 24
  5. def OAI.SKGapCutoff.Primary.previousResidual line 27
  6. lemma OAI.SKGapCutoff.Primary.mag_zero line 30
  7. lemma OAI.SKGapCutoff.Primary.mag_succ line 31
  8. lemma OAI.SKGapCutoff.Primary.onsager_zero line 33
  9. lemma OAI.SKGapCutoff.Primary.fld_eq line 36
  10. lemma OAI.SKGapCutoff.Primary.primary_residual_field line 43
  11. lemma OAI.SKGapCutoff.Primary.residual_inner_product line 54
  12. lemma OAI.SKGapCutoff.Primary.mulVec_pair_symmetric line 67
  13. def OAI.SKGapCutoff.Primary.steinSource line 76
  14. def OAI.SKGapCutoff.Primary.steinPartial line 81
  15. lemma OAI.SKGapCutoff.Primary.stein_residual_pointwise line 86
  16. def OAI.SKGapCutoff.Primary.nextField line 99
  17. theorem OAI.SKGapCutoff.Primary.residual_induction_identity line 107