OAI/Analysis/BernoulliCone/ClampedFoliationGraph.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.Foliation.clampedHeight line 15
2. lemma OAI.Bernoulli.Foliation.le_clampedHeight line 17
3. lemma OAI.Bernoulli.Foliation.clampedHeight_le line 20
4. lemma OAI.Bernoulli.Foliation.below_clampedHeight line 24
5. lemma OAI.Bernoulli.Foliation.above_clampedHeight line 32
6. lemma OAI.Bernoulli.Foliation.graphPotential_eq_integral line 39
7. lemma OAI.Bernoulli.Foliation.clamped_integral_identity line 47
8. lemma OAI.Bernoulli.Foliation.integrated_bulk_open line 66
9. lemma OAI.Bernoulli.Foliation.graphPotential_locallyLipschitz line 79
10. lemma OAI.Bernoulli.Foliation.clamped_split_locallyLipschitz line 86