OAI/NumberTheory/DirichletL/Detector/LowElementRows.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbePhysical.lowElementRowPoint line 14
  2. def OAI.SevenEighths.ProbePhysical.lowIdealRowElement line 17
  3. lemma OAI.SevenEighths.ProbePhysical.lowIdealRowElement_point line 19
  4. lemma OAI.SevenEighths.ProbePhysical.lowElementRowPoint_injective line 22
  5. lemma OAI.SevenEighths.ProbePhysical.lowIdealRowElement_span line 25
  6. lemma OAI.SevenEighths.ProbePhysical.lowElementRowPoint_element line 28
  7. lemma OAI.SevenEighths.ProbePhysical.lowIdealRowElement_norm line 37
  8. def OAI.SevenEighths.ProbePhysical.lowIdealRows line 42
  9. lemma OAI.SevenEighths.ProbePhysical.lowIdealRows_nonzero line 44
  10. lemma OAI.SevenEighths.ProbePhysical.lowIdealRows_norm_bound line 48
  11. theorem OAI.SevenEighths.ProbePhysical.sum_low_element_rows line 53
  12. theorem OAI.SevenEighths.ProbePhysical.low_element_energy_le_units line 77
  13. lemma OAI.SevenEighths.ProbePhysical.low_rowTwist_label_one line 92
  14. lemma OAI.SevenEighths.ProbePhysical.low_units_label_one_sum line 107
  15. lemma OAI.SevenEighths.ProbePhysical.low_element_rowTwist_energy line 114
  16. lemma OAI.SevenEighths.ProbePhysical.lowNumeratorRows_nonzero line 126
  17. lemma OAI.SevenEighths.ProbePhysical.lowNumeratorRows_norm_bound line 133
  18. theorem OAI.SevenEighths.ProbePhysical.lowSelectedInverseRow_ideal_energy line 138
  19. lemma OAI.SevenEighths.ProbePhysical.low_unit_card line 156