OAI/Analysis/BernoulliCone/UpperLeaves.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.upperSigned_pos_zero line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_parameter_continuous line 14
3. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_tendsto_atTop line 21
4. lemma OAI.Bernoulli.DeSilvaJerison.U_le_upperFamily line 29
5. lemma OAI.Bernoulli.DeSilvaJerison.existsUnique_upper_leaf line 34
6. def OAI.Bernoulli.DeSilvaJerison.upperParameter line 61

   Source documentation

   Leaf parameter above the minimizer candidate. Its defining equation is proved from the actual glued DSJ profiles; it is not a new foliation assumption.

   def upperParameter (x:Space 7) (t:ℝ) :ℝ :=
   …

   Mentions: OAI.Bernoulli.Space

7. lemma OAI.Bernoulli.DeSilvaJerison.upperParameter_spec line 63
8. lemma OAI.Bernoulli.DeSilvaJerison.upperParameter_unique line 67
9. lemma OAI.Bernoulli.DeSilvaJerison.upperParameter_lt_iff line 70
10. lemma OAI.Bernoulli.DeSilvaJerison.lt_upperParameter_iff line 83