OAI/Analysis/BernoulliCone/PrimitiveBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.cap_extension_eventually_eq line 12
2. lemma OAI.Bernoulli.DeSilvaJerison.clamped_interior_seam line 22
3. lemma OAI.Bernoulli.DeSilvaJerison.clamped_seam_gradient line 40
4. lemma OAI.Bernoulli.DeSilvaJerison.primitive_eq_split_germ line 53
5. lemma OAI.Bernoulli.DeSilvaJerison.exterior_extension_bulk line 71
6. lemma OAI.Bernoulli.DeSilvaJerison.cap_extension_bulk line 80
7. lemma OAI.Bernoulli.DeSilvaJerison.clamped_extension_jump line 88
8. lemma OAI.Bernoulli.DeSilvaJerison.clamped_extension_bottom line 102
9. theorem OAI.Bernoulli.DeSilvaJerison.upperFlux_primitive_bound line 125

   Source documentation

   Pointwise differential comparison for the genuine discontinuous upper flux primitive, away from the null axis and at differentiability points of its three Lipschitz endpoint graphs.

   theorem upperFlux_primitive_bound {u v:Space 7→ℝ} {x:Space 7}
       (hu:ContinuousAt u x) (hv:ContinuousAt v x) (huv:∀y,u y≤v y)
       (huU:U x<u x) (hqx:0<Cylindrical.radiusSq axis x)
       (hdu:DifferentiableAt ℝ u x) (hdv:DifferentiableAt ℝ v x)
       (hdw:DifferentiableAt ℝ (clampedHeight u seamHeight v) x) :
       divergence (verticalPotential upperFlux u v) x≤
         if u x<v x then ‖gradient v x‖^2+‖upperFlux (x,u x)‖^2-
           2*inner ℝ (upperFlux (x,u x)) (gradient u x) else 0 := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.seamHeight, OAI.Bernoulli.DeSilvaJerison.upperFlux