CapExtension.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_eq_cap line 11
lemma OAI.Bernoulli.DeSilvaJerison.capParameter_local_extension line 21
Source documentation
Smooth signed extensions of the inverse cap parameter through the actual cap/exterior interface, obtained by IFT with local uniqueness.
```
lemma capParameter_local_extension {p:Space 7×ℝ} (hp:U p.1<p.2)
    (hq:Cylindrical.radiusSq axis ((upperParameter p.1 p.2)⁻¹ • p.1)≤1) :
    ∃ψ:Space 7×ℝ→ℝ,ContDiffAt ℝ ∞ ψ p ∧ ψ p=upperParameter p.1 p.2 ∧
      ∀ᶠ z in 𝓝 p, U z.1<z.2 →
        Cylindrical.radiusSq axis ((upperParameter z.1 z.2)⁻¹ • z.1)≤1 →
        ψ z=upperParameter z.1 z.2 := by
…
```
Mentions: OAI.Bernoulli.DeSilvaJerison.p, OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.upperParameter
lemma OAI.Bernoulli.DeSilvaJerison.gradient_smoothCap_contDiffAt line 62
theorem OAI.Bernoulli.DeSilvaJerison.upperFlux_cap_local_extension line 69
Source documentation
The actual one-sided cap flux admits a smooth germ even at the seam. No regularity of the discontinuous full flux is asserted.
```
theorem upperFlux_cap_local_extension {p:Space 7×ℝ} (hp:U p.1<p.2)
    (hq:Cylindrical.radiusSq axis ((upperParameter p.1 p.2)⁻¹ • p.1)≤1) :
    ∃B:Space 7×ℝ→Space 7,ContDiffAt ℝ ∞ B p ∧ B p=upperFlux p ∧
      ∀ᶠ z in 𝓝 p,U z.1<z.2 →
        Cylindrical.radiusSq axis ((upperParameter z.1 z.2)⁻¹ • z.1)≤1 → B z=upperFlux z := by
…
```
Mentions: OAI.Bernoulli.DeSilvaJerison.p, OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.upperParameter, OAI.Bernoulli.DeSilvaJerison.B, OAI.Bernoulli.DeSilvaJerison.upperFlux