OAI/Analysis/BernoulliCone/LocalFluxExtensions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.DeSilvaJerison.exteriorFlux line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.exteriorFlux_contDiffAt line 13
3. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_eq_exterior line 25
4. theorem OAI.Bernoulli.DeSilvaJerison.compact_branch_extensions line 41

   Source documentation

   The actual two branch fields have global C1 representatives on any compact positive-height tube away from the axis. Only the cap-side field is extended from a one-sided region; the full discontinuous flux is never declared smooth.

   theorem compact_branch_extensions {K:Set (Space 7×ℝ)} (hK:IsCompact K)
       (hp:∀p∈K,U p.1<p.2) (hq:∀p∈K,0<Cylindrical.radiusSq axis p.1) :
       ∃A B:Space 7×ℝ→Space 7,ContDiff ℝ 1 A ∧ ContDiff ℝ 1 B ∧
         EqOn A exteriorFlux K ∧
         ∀p∈K,seamHeight p.1≤p.2 → B p=upperFlux p := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.p, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.A, OAI.Bernoulli.DeSilvaJerison.B, OAI.Bernoulli.DeSilvaJerison.exteriorFlux, OAI.Bernoulli.DeSilvaJerison.seamHeight, OAI.Bernoulli.DeSilvaJerison.upperFlux