OAI/Analysis/BernoulliCone/ScalarImplicit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Foliation.real_linear_invertible line 13
2. lemma OAI.Bernoulli.Foliation.scalar_implicit line 31
3. lemma OAI.Bernoulli.Foliation.scalar_implicit_unique line 46

   Source documentation

   The local uniqueness clause of the scalar implicit-function theorem is needed for a smooth extension up to one side of a genuine seam.

   lemma scalar_implicit_unique {F:E×ℝ→ℝ} {x:E} {l ρ:ℝ}
       (hF:ContDiffAt ℝ ∞ F (x,l)) (hd:HasDerivAt (fun s:ℝ=>F (x,s)) ρ l) (hρ:ρ≠0) :
       ∃ψ:E→ℝ, ContDiffAt ℝ ∞ ψ x ∧ ψ x=l ∧
         (∀ᶠ y in 𝓝 x,F (y,ψ y)=F (x,l)) ∧
         ∀ᶠ z in 𝓝 (x,l), F z=F (x,l) ↔ ψ z.1=z.2 := by
   …