OAI/NumberTheory/DirichletL/Moments/SecondBlockAggregate.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentSecondBlockAggregate.ActiveLabel line 25
  2. abbrev OAI.SevenEighths.CenteredMomentSecondBlockAggregate.SourceBlocks line 28
  3. lemma OAI.SevenEighths.CenteredMomentSecondBlockAggregate.retainedRows_ne_zero line 32
  4. theorem OAI.SevenEighths.CenteredMomentSecondBlockAggregate.active_kernel_windows line 37
  5. theorem OAI.SevenEighths.CenteredMomentSecondBlockAggregate.sector_finite_blocks line 56
  6. theorem OAI.SevenEighths.CenteredMomentSecondBlockAggregate.original_secondRetainedEnergy_blocks line 88
  7. lemma OAI.SevenEighths.CenteredMomentSecondBlockAggregate.common_height_norm_le_one line 113
  8. theorem OAI.SevenEighths.CenteredMomentSecondBlockAggregate.original_secondRetainedEnergy_norm_le line 121