Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

The exponential formula is continuous in its increment

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_continuous · theorem · Teaching coverage

Read this first

Mathematical statement

For a fixed base point, the ambient sphere exponential formula depends continuously on z.

\[z_n\to z\Longrightarrow\operatorname{Exp}_w(z_n)\to\operatorname{Exp}_w(z)\]
Lean statement · unitSphereExp_continuous

The conclusion is ordinary topological continuity.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem unitSphereExp_continuous (w : E) : Continuous (unitSphereExp w)

Exact module and namespace context

Proof roadmap

  1. 1Compose continuous operations

    The norm, cosine, sinc, scalar multiplication, and addition are continuous.

Full assumptions and notation

All objects and hypotheses

  • E is a real inner-product space.
  • w is fixed.
  • No tangency premise is needed.

Mathematical proof

1. Compose continuous operations

The norm, cosine, sinc, scalar multiplication, and addition are continuous.

\[z\mapsto\cos(\|z\|)w+\operatorname{sinc}(\|z\|)z\]
Corresponding Lean step

After unfolding, fun_prop applies Mathlib's continuity rules.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphereExp_continuous

The proof is a direct closure argument.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem unitSphereExp_continuous (w : E) : Continuous (unitSphereExp w) := by
  unfold unitSphereExp
  fun_prop

Exact module and namespace context

Scope and omitted-condition boundaries
  • Joint differentiability in both arguments is not claimed.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    No direct Mathlib call recorded; see the Samplinglib parents.

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.