OAI/Analysis/BernoulliCone/PrimitiveLocal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Bernoulli.DeSilvaJerison.above_U_isOpen line 12
  2. lemma OAI.Bernoulli.DeSilvaJerison.capTube_isOpen line 15
  3. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_primitive_axis_lipschitz line 25
  4. lemma OAI.Bernoulli.DeSilvaJerison.seamHeight_smooth_germ line 40
  5. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_compact_tube line 49
  6. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_primitive_offaxis_lipschitz line 63
  7. theorem OAI.Bernoulli.DeSilvaJerison.upperFlux_primitive_locallyLipschitz line 85

    Source documentation

    The actual discontinuous calibration has a locally Lipschitz vertical primitive whenever its endpoints stay strictly above U. This includes the axis and the vertex, not just the smooth off-interface regions.

    theorem upperFlux_primitive_locallyLipschitz {u v:Space 7→ℝ}
    (hu:LocallyLipschitz u) (hv:LocallyLipschitz v) (huv:∀y,u y≤v y)
    (huU:∀y,U y<u y) : LocallyLipschitz (verticalPotential upperFlux u v) := by
…

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