Analytic

Results named in Tau Ceti's TauCeti.Analysis.Analytic modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe analytic implicit function theorem#

If f : E₁ × E → F is analytic at u and its partial derivative in the second variable is invertible there, the implicit function ψ with f (x, ψ x) = f u near u.1 is analytic at u.1.

HasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
  {E₁ : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [CompleteSpace E₁] {f : E₁ × E → F}
  {f'u : E₁ × E →L[𝕜] F} {u : E₁ × E} (dfu : HasStrictFDerivAt f f'u u)
  (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E).IsInvertible) (hf : AnalyticAt 𝕜 f u) :
  AnalyticAt 𝕜 (dfu.implicitFunctionOfProdDomain if₂u) u.1

Lean

Formalized in Tau Ceti as HasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain.

Other forms

The analytic implicit function theorem, general form. Formalized in Tau Ceti as ImplicitFunctionData.analyticAt_implicitFunction.

ImplicitFunctionData.analyticAt_implicitFunction.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
  {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G]
  {φ : ImplicitFunctionData 𝕜 E F G} (hl : AnalyticAt 𝕜 φ.leftFun φ.pt)
  (hr : AnalyticAt 𝕜 φ.rightFun φ.pt) :
  AnalyticAt 𝕜 (Function.uncurry φ.implicitFunction) (φ.prodFun φ.pt)

Sources

• Tau Ceti documentation: HasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain
• Source of HasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain in TauCeti/Analysis/Analytic/Inverse.lean

LeanHasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain · ImplicitFunctionData.analyticAt_implicitFunction

Used by 3

Used byThe analytic implicit root theorem · The joint holomorphic implicit function theorem · Nash implicit function theorem for systems

TheoremThe analytic implicit root theorem#

Let f (w, z) be analytic at u = (w₀, z₀), with f u = 0 and ∂f/∂z ≠ 0 at u. Then there is a function g, analytic at w₀ with g w₀ = z₀, such that near u the zeros of f are exactly the points (w, g w); in particular f (w, g w) = 0 for all w near w₀.

AnalyticAt.exists_analyticAt_eventually_eq_zero_iff.{u_1, u_2} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] [CompleteSpace 𝕜] {f : E × 𝕜 → 𝕜} {u : E × 𝕜} (hf : AnalyticAt 𝕜 f u)
  (hu : f u = 0) (h : deriv (fun z => f (u.1, z)) u.2 ≠ 0) :
  ∃ g,
    AnalyticAt 𝕜 g u.1 ∧
      g u.1 = u.2 ∧
        (∀ᶠ (w : E) in nhds u.1, f (w, g w) = 0) ∧ ∀ᶠ (v : E × 𝕜) in nhds u, f v = 0 ↔ g v.1 = v.2

Lean

Formalized in Tau Ceti as AnalyticAt.exists_analyticAt_eventually_eq_zero_iff.

Sources

• Tau Ceti documentation: AnalyticAt.exists_analyticAt_eventually_eq_zero_iff
• Source of AnalyticAt.exists_analyticAt_eventually_eq_zero_iff in TauCeti/Analysis/Analytic/Inverse.lean

LeanAnalyticAt.exists_analyticAt_eventually_eq_zero_iff

Uses 1 · Used by 8

Proof usesThe analytic implicit function theorem

Used byThe superelliptic curve is the analytic Belyi pair of the torus triple · Analytic delineability from constant discriminant order · CAD lifting by Lazard delineations in a reordered base · Correctness of McCallum's projection · Lazard lifting of a family · Recursive sign-invariant McCallum correctness · Sign-invariance of the McCallum projection does not suffice for lifting · The Nash implicit root theorem

TheoremThe analytic inverse function theorem#

A map analytic at a, whose derivative at a is a continuous linear equivalence, coincides with an OpenPartialHomeomorph whose source is a neighbourhood of a inside any prescribed neighbourhood s, which is analytic on its source, and whose inverse is analytic on its target.

AnalyticAt.exists_openPartialHomeomorph.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {a : E} (hf : AnalyticAt 𝕜 f a)
  {L : E ≃L[𝕜] F} (hL : fderiv 𝕜 f a = ↑L) {s : Set E} (hs : s ∈ nhds a) :
  ∃ Θ,
    ↑Θ = f ∧
      a ∈ Θ.source ∧ Θ.source ⊆ s ∧ AnalyticOnNhd 𝕜 f Θ.source ∧ AnalyticOnNhd 𝕜 (↑Θ.symm) Θ.target

Lean

Formalized in Tau Ceti as AnalyticAt.exists_openPartialHomeomorph.

Sources

• Tau Ceti documentation: AnalyticAt.exists_openPartialHomeomorph
• Source of AnalyticAt.exists_openPartialHomeomorph in TauCeti/Analysis/Analytic/Inverse.lean

LeanAnalyticAt.exists_openPartialHomeomorph

Used by 3

Used byAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · The superelliptic curve is the analytic Belyi pair of the torus triple · The Nash inverse function theorem

TheoremHadamard's lemma along a graph#

a function G analytic at (x₀, g x₀) that vanishes on the graph y = g x of a function g analytic at x₀ is (y - g x) • H (x, y) near (x₀, g x₀), with H analytic at (x₀, g x₀).

AnalyticAt.exists_eventuallyEq_sub_smul_of_graph.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] [CompleteSpace F] {G : E × 𝕜 → F} {g : E → 𝕜} {x₀ : E}
  (hG : AnalyticAt 𝕜 G (x₀, g x₀)) (hg : AnalyticAt 𝕜 g x₀)
  (h0 : ∀ᶠ (x : E) in nhds x₀, G (x, g x) = 0) :
  ∃ H, AnalyticAt 𝕜 H (x₀, g x₀) ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, g x₀), G p = (p.2 - g p.1) • H p

Lean

Formalized in Tau Ceti as AnalyticAt.exists_eventuallyEq_sub_smul_of_graph.

Other forms

Hadamard's lemma for analytic functions. Formalized in Tau Ceti as AnalyticAt.exists_analyticAt_eventually_sub_eq.

AnalyticAt.exists_analyticAt_eventually_sub_eq.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : E} (hf : AnalyticAt 𝕜 f c) :
  ∃ G, AnalyticAt 𝕜 G c ∧ G c = fderiv 𝕜 f c ∧ ∀ᶠ (z : E) in nhds c, f z - f c = (G z) (z - c)

Hadamard's lemma in a distinguished variable. Formalized in Tau Ceti as AnalyticAt.exists_eventuallyEq_sub_smul.

AnalyticAt.exists_eventuallyEq_sub_smul.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  [CompleteSpace F] {G : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} (hG : AnalyticAt 𝕜 G (x₀, y₀))
  (h0 : ∀ᶠ (x : E) in nhds x₀, G (x, y₀) = 0) :
  ∃ H, AnalyticAt 𝕜 H (x₀, y₀) ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), G p = (p.2 - y₀) • H p

Sources

• Tau Ceti documentation: AnalyticAt.exists_eventuallyEq_sub_smul_of_graph
• Source of AnalyticAt.exists_eventuallyEq_sub_smul_of_graph in TauCeti/Analysis/Analytic/ConstantOrder/Basic.lean

LeanAnalyticAt.exists_eventuallyEq_sub_smul_of_graph · AnalyticAt.exists_analyticAt_eventually_sub_eq · AnalyticAt.exists_eventuallyEq_sub_smul

Used by 6

Used byHadamard's lemma in coordinates · Analytic delineability from constant discriminant order · Correctness of McCallum's projection · Lazard lifting of a family · Recursive sign-invariant McCallum correctness · Sign-invariance of the McCallum projection does not suffice for lifting

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.