OAI/NumberTheory/DirichletL/Detector/GaussianCompensation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbePhysical.physicalElementNorm_pos line 14
2. lemma OAI.SevenEighths.ProbePhysical.elementNorm_slotProduct line 19
3. lemma OAI.SevenEighths.ProbePhysical.slotProduct_nonzero line 25
4. lemma OAI.SevenEighths.ProbePhysical.slotProduct_norm_pos line 28
5. def OAI.SevenEighths.ProbePhysical.compensationSubsetCoefficient line 31
6. def OAI.SevenEighths.ProbePhysical.compensationSubsetProbe line 36
7. lemma OAI.SevenEighths.ProbePhysical.compensatedTuple_eq_subsets line 43
8. lemma OAI.SevenEighths.ProbePhysical.compensatedPhysicalProbe_eq_subsets line 48
9. theorem OAI.SevenEighths.ProbePhysical.compensationSubsetProbe_eq_gaussian_rows line 60