OAI/Analysis/BernoulliCone/HalfspaceDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.Shape.density line 14
2. def OAI.Bernoulli.Shape.firstTerm line 16
3. lemma OAI.Bernoulli.Shape.density_nonneg line 19
4. lemma OAI.Bernoulli.Shape.gradient_norm_le_lipschitz line 23
5. lemma OAI.Bernoulli.Shape.density_pullback_bound line 29