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

CurveExtension: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Why the derivative along a feasible curve ignores the extension
Samplinglib mathematical lesson

Why the derivative along a feasible curve ignores the extension

AutoSamplingTheory.TechnicalLemmas.Geometry.CurveExtension.fderiv_eq_on_curve_velocity · theorem · Teaching coverage

Read this first

Mathematical statement

Let E and V be real normed spaces, s⊆E, and f,g:E→V. At x=c(t₀), suppose f and g are genuinely differentiable, c has actual velocity v, c(t) lies in s for all t sufficiently near t₀, and f=g locally relative to s at x. Then Df(x)[v]=Dg(x)[v].

\[x=c(t_0),\quad c\prime(t_0)=v,\qquad Df(x)[v]=Dg(x)[v].\]
Lean statement · fderiv_eq_on_curve_velocity

DifferentiableAt certifies both ambient derivatives; HasDerivAt certifies the actual curve velocity. Eventually in 𝓝 means locally near t₀. EventuallyEq in 𝓝[s] x means equality on a relative neighborhood. E→V are total Lean function types, but only their local germs enter this proof.

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 fderiv_eq_on_curve_velocity
    {s : Set E} {f g : E → F} {c : ℝ → E} {t₀ : ℝ} {v : E}
    (hf : DifferentiableAt ℝ f (c t₀))
    (hg : DifferentiableAt ℝ g (c t₀))
    (hc : HasDerivAt c v t₀)
    (hcs : ∀ᶠ t in 𝓝 t₀, c t ∈ s)
    (hfg : f =ᶠ[𝓝[s] (c t₀)] g) :
    fderiv ℝ f (c t₀) v = fderiv ℝ g (c t₀) v

Exact module and namespace context

Proof roadmap

  1. 1Pull the agreement back to the curve

    A differentiable curve is continuous. Together with local feasibility, continuity sends sufficiently small parameter neighborhoods into relative neighborhoods of x in s. The two image curves therefore agree near t₀. This is a local argument: neither extension needs to agree off the feasible set.

  2. 2Differentiate each image curve

    Apply the actual chain rule to each genuinely differentiable ambient map and the actual curve derivative. Its velocity is the ambient derivative applied to v. This derives both image derivatives inside the proof.

  3. 3Use locality and uniqueness

    Locally equal image curves share their derivative at t₀. Transfer the first derivative witness to the second image curve; uniqueness then equates the two velocities. For every source tangent vector represented by a smooth feasible curve, this gives the extension-choice equality. The remaining manifold tangent adapter must be supplied separately.

Full assumptions and notation

All objects and hypotheses

  • E and V are real normed spaces, possibly infinite-dimensional and incomplete. No chosen Riemannian metric, inner product, Riesz gradient, orthogonal projector or manifold structure is required. This generalizes the finite-dimensional Euclidean source proof ingredient.
  • Both ambient maps have genuine pointwise Fréchet derivatives at x. Smoothness of the source extensions implies this condition. fderiv is not used to manufacture a derivative when none exists.
  • c:ℝ→E has a genuine derivative v at t₀ and lies locally in s. Source smooth manifold curves satisfy these weaker local requirements.
  • The two ambient maps agree on some relative neighborhood of x in s. They need not agree in any open ambient neighborhood. Source neighborhood extensions of the same manifold map supply this equality locally.

Mathematical proof

1. Pull the agreement back to the curve

A differentiable curve is continuous. Together with local feasibility, continuity sends sufficiently small parameter neighborhoods into relative neighborhoods of x in s. The two image curves therefore agree near t₀. This is a local argument: neither extension needs to agree off the feasible set.

\[f(c(t))=g(c(t))\quad\text{for all }t\text{ sufficiently near }t_0.\]
Corresponding Lean step
  have hcts : Tendsto c (𝓝 t₀) (𝓝[s] (c t₀)) :=
    tendsto_nhdsWithin_iff.mpr ⟨hc.continuousAt, hcs⟩
  have hcomp : (f ∘ c) =ᶠ[𝓝 t₀] (g ∘ c) := hfg.comp_tendsto hcts

HasDerivAt.continuousAt and tendsto_nhdsWithin_iff construct the relative-neighborhood limit. Filter.EventuallyEq.comp_tendsto pulls back local equality.

2. Differentiate each image curve

Apply the actual chain rule to each genuinely differentiable ambient map and the actual curve derivative. Its velocity is the ambient derivative applied to v. This derives both image derivatives inside the proof.

\[(f\circ c)\prime(t_0)=Df(x)[v],\qquad (g\circ c)\prime(t_0)=Dg(x)[v].\]
Corresponding Lean step
  have hfc := hf.hasFDerivAt.comp_hasDerivAt t₀ hc
  have hgc := hg.hasFDerivAt.comp_hasDerivAt t₀ hc

DifferentiableAt.hasFDerivAt gives a real derivative witness; HasFDerivAt.comp_hasDerivAt is the Fréchet/one-parameter chain rule.

3. Use locality and uniqueness

Locally equal image curves share their derivative at t₀. Transfer the first derivative witness to the second image curve; uniqueness then equates the two velocities. For every source tangent vector represented by a smooth feasible curve, this gives the extension-choice equality. The remaining manifold tangent adapter must be supplied separately.

\[Df(x)[v]=(f\circ c)\prime(t_0)=(g\circ c)\prime(t_0)=Dg(x)[v].\]
Corresponding Lean step
  exact (hfc.congr_of_eventuallyEq hcomp.symm).unique hgc

HasDerivAt.congr_of_eventuallyEq transfers the witness. HasDerivAt.unique compares two genuine derivatives of one image curve.

Lean verification

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

Lean proof · fderiv_eq_on_curve_velocity

Pull relative equality back by the continuous feasible curve, apply the two genuine chain rules, then compare derivatives by locality and uniqueness.

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 fderiv_eq_on_curve_velocity
    {s : Set E} {f g : E → F} {c : ℝ → E} {t₀ : ℝ} {v : E}
    (hf : DifferentiableAt ℝ f (c t₀))
    (hg : DifferentiableAt ℝ g (c t₀))
    (hc : HasDerivAt c v t₀)
    (hcs : ∀ᶠ t in 𝓝 t₀, c t ∈ s)
    (hfg : f =ᶠ[𝓝[s] (c t₀)] g) :
    fderiv ℝ f (c t₀) v = fderiv ℝ g (c t₀) v := by
  have hcts : Tendsto c (𝓝 t₀) (𝓝[s] (c t₀)) :=
    tendsto_nhdsWithin_iff.mpr ⟨hc.continuousAt, hcs⟩
  have hcomp : (f ∘ c) =ᶠ[𝓝 t₀] (g ∘ c) := hfg.comp_tendsto hcts
  have hfc := hf.hasFDerivAt.comp_hasDerivAt t₀ hc
  have hgc := hg.hasFDerivAt.comp_hasDerivAt t₀ hc
  exact (hfc.congr_of_eventuallyEq hcomp.symm).unique hgc

end AutoSamplingTheory.TechnicalLemmas.Geometry.CurveExtension

Exact module and namespace context

Scope and omitted-condition boundaries
  • This proves the actual nonlinear-curve extension-independence edge. It does not identify the full embedded-manifold differential, prove its tangent-space domain/codomain adapter or complete Proposition3.35/3.61.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • tendsto_nhdsWithin_iff
    • HasDerivAt.continuousAt
    • Filter.EventuallyEq.comp_tendsto
    • DifferentiableAt.hasFDerivAt
    • HasFDerivAt.comp_hasDerivAt
    • HasDerivAt.congr_of_eventuallyEq
    • HasDerivAt.unique

    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.