OAI/NumberTheory/DirichletL/Moments/AmplificationChildSourceCaps.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.geometry line 22
  2. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.geometry_ge_one line 24
  3. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.norm_ge_one line 31
  4. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.allocation_product line 34
  5. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.allocation_ne line 37
  6. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.common_volume line 41
  7. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.live_card_le line 55
  8. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.common_volume_le line 58
  9. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.frozen_zero line 76
  10. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.radius_le line 80
  11. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.original_beta line 100
  12. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.child_column_norm line 103
  13. def OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.nominal line 111
  14. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.nominal_pos line 113
  15. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.nominal_lower line 116
  16. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.nominal_upper line 119
  17. def OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.Endpoints line 125
  18. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.endpoints_child line 128
  19. lemma OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.radius_bound line 133
  20. def OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twiceChild line 141
  21. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twiceChild_data line 146
  22. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twice_volume line 154
  23. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twice_caps line 162
  24. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twice_column line 199
  25. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twice_nominal line 214
  26. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.puncture_norm line 229
  27. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.live_puncture_bound line 233
  28. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.eventual_geometry line 257
  29. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.polynomial_caps line 263
  30. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.eventual_twice_caps line 292
  31. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.plain_zero line 328
  32. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.twice_slots_ge_one line 335
  33. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.child_localized line 341
  34. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.child_source_zero line 356
  35. theorem OAI.SevenEighths.CenteredMomentAmplificationChildSourceCaps.eventual_live_puncture line 369