OAI/Probability/GaussianInformation/Inverse/Tubes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AllScaleInverseVolume.synth line 10
2. def OAI.AllScaleInverseVolume.coordinates line 12
3. def OAI.AllScaleInverseVolume.residual line 14
4. lemma OAI.AllScaleInverseVolume.synth_norm line 17
5. lemma OAI.AllScaleInverseVolume.synth_sub line 25
6. lemma OAI.AllScaleInverseVolume.synth_smul line 28
7. def OAI.AllScaleInverseVolume.groupedTube line 32
8. lemma OAI.AllScaleInverseVolume.exists_groupedTube_cover line 36
9. lemma OAI.AllScaleInverseVolume.measure_groupedTube_le line 80