OAI/Computability/MinUncut/Analysis/GaussianAssembly.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncut.BoxGaussian.singletonEmbed line 13
2. lemma OAI.MinUncut.BoxGaussian.singletonEmbed_injective line 15
3. lemma OAI.MinUncut.BoxGaussian.update_join_singleton line 20
4. lemma OAI.MinUncut.BoxGaussian.integral_singleton line 34
5. lemma OAI.MinUncut.BoxGaussian.centered_resample_memLp line 39
6. lemma OAI.MinUncut.BoxGaussian.integral_split_le line 72
7. lemma OAI.MinUncut.BoxGaussian.centered_resample_loss line 87