OAI/Analysis/BernoulliCone/PositiveTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.U_lt_upperFamily line 10
2. lemma OAI.Bernoulli.DeSilvaJerison.U_pos_radiusSq line 15
3. lemma OAI.Bernoulli.DeSilvaJerison.upperParameter_eventually_outer line 21
4. lemma OAI.Bernoulli.DeSilvaJerison.U_eq_signed_of_pos line 34
5. lemma OAI.Bernoulli.DeSilvaJerison.gradient_U_eq_signed line 41
6. lemma OAI.Bernoulli.DeSilvaJerison.normalized_radiusSq_ne_one line 48
7. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_outer_affine line 57
8. theorem OAI.Bernoulli.DeSilvaJerison.upperFlux_tendsto_positive_trace line 65

   Source documentation

   The actual bounded field has the exact positive-phase lower trace.

   theorem upperFlux_tendsto_positive_trace {x:Space 7} (hx:0<U x) :
       Tendsto (fun t:ℝ=>upperFlux (x,t)) (𝓝[>] (U x)) (𝓝 (gradient U x)) := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.DeSilvaJerison.upperFlux