A machine-checked solution to the Jacobians challenge

7.8. Path.SmoothPath🔗

Jacobians.Path.SmoothPath — source

ChartBallPath

Chart-ball-linear path. Linear interpolation in the chart at P, pulled back to X. Pre-conditions are not encoded in the type; the auxiliary lemmas below assume P ∈ c.source, Q ∈ c.source, and that the linear interpolation (1 - (t : ℂ)) * c P + (t : ℂ) * c Q stays in c.target for t ∈ [0,1] (any convex subset of c.target containing c P and c Q suffices).

noncomputable def ChartBallPath {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (anchor P Q : X)
    : ℝ → X

ChartBallPath.start

The chart-ball-linear path at t = 0 is P, when P is in the chart's source.

@[simp] lemma ChartBallPath.start {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor P Q : X)
    (hP : P ∈ (chartAt ℂ anchor).source) :
    ChartBallPath anchor P Q 0 = P

ChartBallPath.finish

The chart-ball-linear path at t = 1 is Q, when Q is in the chart's source.

@[simp] lemma ChartBallPath.finish {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor P Q : X)
    (hQ : Q ∈ (chartAt ℂ anchor).source) :
    ChartBallPath anchor P Q 1 = Q

ChartBallPath.continuousOn

The chart-ball-linear path is continuous on [0,1], provided the linear interpolation stays in the chart's open target.

lemma ChartBallPath.continuousOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor P Q : X)
    (h : ∀ t ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)
        ∈ (chartAt ℂ anchor).target) :
    ContinuousOn (ChartBallPath anchor P Q) (Set.Icc 0 1)

smoothStep01

The cubic 3t² - 2t³ smoothstep, clamped to [0,1].

noncomputable def smoothStep01 (t : ℝ) : ℝ

smoothStep01_zero

@[simp] lemma smoothStep01_zero : smoothStep01 0 = 0

smoothStep01_one

@[simp] lemma smoothStep01_one : smoothStep01 1 = 1

smoothStep01_of_mem_open

smoothStep01 agrees with 3t² - 2t³ on the open interval (0, 1).

lemma smoothStep01_of_mem_open (t : ℝ) (h0 : 0 < t) (h1 : t < 1) :
    smoothStep01 t = 3 * t^2 - 2 * t^3

smoothStep01_eqOn_one

smoothStep01 is locally constant for t > 1.

lemma smoothStep01_eqOn_one : Set.EqOn smoothStep01 (fun _ => (1 : ℝ)) (Set.Ioi 1)

smoothStep01_eqOn_zero

smoothStep01 is locally constant for t < 0.

lemma smoothStep01_eqOn_zero : Set.EqOn smoothStep01 (fun _ => (0 : ℝ)) (Set.Iio 0)

smoothStep01_nonneg

The smoothstep is bounded between 0 and 1 globally.

lemma smoothStep01_nonneg (t : ℝ) : 0 ≤ smoothStep01 t

smoothStep01_le_one

lemma smoothStep01_le_one (t : ℝ) : smoothStep01 t ≤ 1

chart_ChartBallPath_eq

The chart-coords formula (chartAt ℂ anchor) (ChartBallPath anchor P Q t) on the inverse domain: when (1-t)*cP + t*cQ ∈ chart.target, the chart inverse-applied-then-chart-applied is identity.

lemma chart_ChartBallPath_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (anchor P Q : X)
    (t : ℝ)
    (h_in_target :
      ((1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)
        ∈ (chartAt ℂ anchor).target) :
    (chartAt ℂ anchor) (ChartBallPath anchor P Q t) =
      (1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q

continuous_chart_image_formula

lemma continuous_chart_image_formula {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor P Q : X) :
    Continuous
      (fun t : ℝ => (1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)

differentiable_chart_image_formula

lemma differentiable_chart_image_formula {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor P Q : X) :
    Differentiable ℝ
      (fun t : ℝ => (1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)

ChartBallPath_mem_source

The ChartBallPath at t lies in the chart source if the affine chart-image formula stays in the chart target.

lemma ChartBallPath_mem_source {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (anchor P Q : X)
    (t : ℝ)
    (h_in_target :
      ((1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)
        ∈ (chartAt ℂ anchor).target) :
    ChartBallPath anchor P Q t ∈ (chartAt ℂ anchor).source

smoothStep01_mem_unit

smoothStep01 t ∈ [0, 1] for any t.

lemma smoothStep01_mem_unit (t : ℝ) : smoothStep01 t ∈ Set.Icc (0 : ℝ) 1

smoothStep01_at_quarter

smoothStep01 at integer multiples of 1/n. (Doesn't always equal k/n — smoothstep is non-linear on (0, 1).)

lemma smoothStep01_at_quarter : smoothStep01 (1 / 4) = 5 / 32

smoothStep01_at_three_quarter

lemma smoothStep01_at_three_quarter : smoothStep01 (3 / 4) = 27 / 32

smoothStep01_continuous

smoothStep01 is globally continuous on ℝ.

Built via Continuous.if: branches agree on the frontier (at t = 0, both equal 0; at t = 1, both equal 1).

lemma smoothStep01_continuous : Continuous smoothStep01

smoothStep01_hasDerivAt_zero

smoothStep01 has derivative 0 at t = 0 (zero on both sides).

lemma smoothStep01_hasDerivAt_zero : HasDerivAt smoothStep01 0 0

smoothStep01_hasDerivAt_one

smoothStep01 has derivative 0 at t = 1 (zero on both sides).

lemma smoothStep01_hasDerivAt_one : HasDerivAt smoothStep01 0 1

smoothStep01_deriv

Explicit derivative of smoothStep01: 0 outside (0, 1), 6t(1-t) on (0, 1), also 0 at the boundary points (matching zero left/right derivatives).

noncomputable def smoothStep01_deriv (t : ℝ) : ℝ

smoothStep01_deriv_zero

@[simp] lemma smoothStep01_deriv_zero : smoothStep01_deriv 0 = 0

smoothStep01_deriv_one

@[simp] lemma smoothStep01_deriv_one : smoothStep01_deriv 1 = 0

smoothStep01_deriv_eqOn_zero

lemma smoothStep01_deriv_eqOn_zero :
    Set.EqOn smoothStep01_deriv (fun _ : ℝ => 0) (Set.Iio 0)

smoothStep01_deriv_eqOn_one

lemma smoothStep01_deriv_eqOn_one :
    Set.EqOn smoothStep01_deriv (fun _ : ℝ => 0) (Set.Ioi 1)

smoothStep01_deriv_eqOn_open

lemma smoothStep01_deriv_eqOn_open :
    Set.EqOn smoothStep01_deriv (fun t => 6 * t * (1 - t)) (Set.Ioo (0 : ℝ) 1)

smoothStep01_hasDerivAt_explicit

HasDerivAt at each t ∈ ℝ for smoothStep01 with explicit derivative smoothStep01_deriv t.

lemma smoothStep01_hasDerivAt_explicit (t : ℝ) :
    HasDerivAt smoothStep01 (smoothStep01_deriv t) t

smoothStep01_deriv_continuous

smoothStep01_deriv is continuous globally.

lemma smoothStep01_deriv_continuous : Continuous smoothStep01_deriv

smoothStep01_deriv_continuousOn_uIcc

smoothStep01_deriv is ContinuousOn uIcc 0 1 — corollary of global continuity. Specialized for use with intervalIntegral.integral_deriv_smul_comp'.

lemma smoothStep01_deriv_continuousOn_uIcc :
    ContinuousOn smoothStep01_deriv (Set.uIcc (0 : ℝ) 1)

smoothStep01_deriv_nonneg_on_Icc

smoothStep01_deriv is nonneg on [0, 1].

lemma smoothStep01_deriv_nonneg_on_Icc {t : ℝ} (_ht : t ∈ Set.Icc (0 : ℝ) 1) :
    0 ≤ smoothStep01_deriv t

smoothStep01_differentiable

smoothStep01 is globally Differentiable ℝ, with derivative 0 at boundary and 6t(1-t) on (0, 1).

lemma smoothStep01_differentiable : Differentiable ℝ smoothStep01

smoothStep01_monotoneOn_Icc

smoothStep01 is monotone on [0, 1].

lemma smoothStep01_monotoneOn_Icc :
    MonotoneOn smoothStep01 (Set.Icc (0 : ℝ) 1)

smoothStep01_image_Icc

smoothStep01 maps [0, 1] onto [0, 1] (image).

lemma smoothStep01_image_Icc :
    smoothStep01 '' Set.Icc (0 : ℝ) 1 = Set.Icc (0 : ℝ) 1

ChartBallPathSmooth

Smoothstep-reparameterized chart-ball path. Maps ℝ → X by composing ChartBallPath Q₀ Q₀ Q with smoothStep01. Globally continuous (since smoothStep01 maps ℝ → [0, 1] and ChartBallPath is ContinuousOn [0, 1]).

noncomputable def ChartBallPathSmooth {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (Q₀ Q : X)
    : ℝ → X

ChartBallPathSmooth.start

ChartBallPathSmooth Q₀ Q 0 = Q₀ when Q₀ is in the chart source.

@[simp] lemma ChartBallPathSmooth.start {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (Q₀ Q : X)
    (hQ₀_src : Q₀ ∈ (chartAt (H := ℂ) Q₀).source) :
    ChartBallPathSmooth Q₀ Q 0 = Q₀

ChartBallPathSmooth.finish

ChartBallPathSmooth Q₀ Q 1 = Q when Q is in the chart source.

@[simp] lemma ChartBallPathSmooth.finish {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (Q₀ Q : X)
    (hQ_src : Q ∈ (chartAt (H := ℂ) Q₀).source) :
    ChartBallPathSmooth Q₀ Q 1 = Q

ChartBallPathSmooth.continuous

ChartBallPathSmooth Q₀ Q is globally continuous on ℝ, provided the chart-ball hypothesis holds on [0, 1].

lemma ChartBallPathSmooth.continuous {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (Q₀ Q : X)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) Q₀) Q₀ +
        (s : ℂ) * (chartAt (H := ℂ) Q₀) Q) ∈ (chartAt (H := ℂ) Q₀).target) :
    Continuous (ChartBallPathSmooth Q₀ Q)

anchor_mem_chart_source

Anchor is always in its own chart's source.

@[simp] lemma anchor_mem_chart_source {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor : X) : anchor ∈ (chartAt ℂ anchor).source

chartAt_anchor_in_target

chartAt anchor anchor is in chartAt anchor.target.

@[simp] lemma chartAt_anchor_in_target {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor : X) :
    (chartAt ℂ anchor) anchor ∈ (chartAt ℂ anchor).target

chart_transition_contDiffOn

Chart transitions on an analytic complex manifold are ContDiffOn ℂ ω. For any two points x, y : X, the trans (chartAt ℂ x).symm ≫ₕ (chartAt ℂ y) is in the contDiffGroupoid ω 𝓘(ℂ), giving its underlying function as ContDiffOn ℂ ω on the trans's source.

lemma chart_transition_contDiffOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x y : X) :
    let e : OpenPartialHomeomorph ℂ ℂ

chart_transition_contDiffOn_simplified

For self-model 𝓘(ℂ), the ModelWithCorners coercion is identity, so the ContDiffOn statement above simplifies to plain ContDiffOn ℂ ω of the chart transition function on its source.

lemma chart_transition_contDiffOn_simplified {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x y : X) :
    let e : OpenPartialHomeomorph ℂ ℂ

chart_trans_source_iff

Chart transition source membership: u is in the trans source iff u ∈ (chartAt ℂ x).target and (chartAt ℂ x).symm u ∈ (chartAt ℂ y).source.

lemma chart_trans_source_iff {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x y : X) (u : ℂ) :
    u ∈ ((chartAt ℂ x).symm ≫ₕ (chartAt ℂ y)).source ↔
      u ∈ (chartAt ℂ x).target ∧ (chartAt ℂ x).symm u ∈ (chartAt ℂ y).source

chart_transition_contDiffAt

Chart transition is ContDiffAt ℂ ω at every point in its source.

lemma chart_transition_contDiffAt {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x y : X) (u : ℂ)
    (h_target : u ∈ (chartAt ℂ x).target)
    (h_source : (chartAt ℂ x).symm u ∈ (chartAt ℂ y).source) :
    ContDiffAt ℂ ω (((chartAt ℂ x).symm ≫ₕ (chartAt ℂ y)) : ℂ → ℂ) u

chart_transition_differentiableAt_C

Chart transition is DifferentiableAt ℂ at every point in its source.

lemma chart_transition_differentiableAt_C {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x y : X) (u : ℂ)
    (h_target : u ∈ (chartAt ℂ x).target)
    (h_source : (chartAt ℂ x).symm u ∈ (chartAt ℂ y).source) :
    DifferentiableAt ℂ (((chartAt ℂ x).symm ≫ₕ (chartAt ℂ y)) : ℂ → ℂ) u

instIsScalarTower_R_C_C

IsScalarTower ℝ ℂ ℂ: trivial via the Complex.smul_def / IsScalarTower.right-style construction. Stated locally to make restrictScalars ℝ synthesis succeed.

instance instIsScalarTower_R_C_C : IsScalarTower ℝ ℂ ℂ

chart_transition_differentiableAt_R

Chart transition is DifferentiableAt ℝ (restrict-scalars from ℂ to ℝ). We pass the IsScalarTower ℝ ℂ ℂ instance explicitly because Lean's typeclass search doesn't pick it up automatically inside our namespace

  • variable-block context.

lemma chart_transition_differentiableAt_R {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x y : X) (u : ℂ)
    (h_target : u ∈ (chartAt ℂ x).target)
    (h_source : (chartAt ℂ x).symm u ∈ (chartAt ℂ y).source) :
    DifferentiableAt ℝ (((chartAt ℂ x).symm ≫ₕ (chartAt ℂ y)) : ℂ → ℂ) u

chart_transition_comp_differentiableAt_R

Chart transition as plain function composition (chartAt ℂ y) ∘ (chartAt ℂ x).symm is DifferentiableAt ℝ at u. Rewriting OpenPartialHomeomorph.trans as plain function composition.

lemma chart_transition_comp_differentiableAt_R {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x y : X) (u : ℂ)
    (h_target : u ∈ (chartAt ℂ x).target)
    (h_source : (chartAt ℂ x).symm u ∈ (chartAt ℂ y).source) :
    DifferentiableAt ℝ (fun v : ℂ => (chartAt ℂ y) ((chartAt ℂ x).symm v)) u

ChartBallPath_chart_at_self_differentiableAt

The chart-pullback of ChartBallPath via the chart at γ t is DifferentiableAt ℝ at t, provided the affine z t is in the chart at anchor's target.

lemma ChartBallPath_chart_at_self_differentiableAt {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (anchor P Q : X) (t : ℝ)
    (h_target_at_t : ((1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)
      ∈ (chartAt ℂ anchor).target) :
    DifferentiableAt ℝ
      ((chartAt (H := ℂ) (ChartBallPath anchor P Q t)).toFun ∘ ChartBallPath anchor P Q) t

ChartBallPathSmooth_chart_at_self_differentiableAt

Chart-pullback differentiability of ChartBallPathSmooth at each t.

By chain rule: (chartAt (γt)) ∘ ChartBallPathSmooth = ((chartAt (γt)) ∘ ChartBallPath) ∘ smoothStep01. The inner composition is diff at smoothStep01 t (provided chart-ball at that point — follows from smoothStep01 t ∈ [0, 1]). Outer composition with smoothStep01 (differentiable everywhere) gives diff at t.

lemma ChartBallPathSmooth_chart_at_self_differentiableAt {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ Q : X) (t : ℝ)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) Q₀) Q₀ +
        (s : ℂ) * (chartAt (H := ℂ) Q₀) Q) ∈ (chartAt (H := ℂ) Q₀).target) :
    DifferentiableAt ℝ
      ((chartAt (H := ℂ) (ChartBallPathSmooth Q₀ Q t)).toFun ∘ ChartBallPathSmooth Q₀ Q) t

ChartBallPath_continuousOn_target_set

Continuity of ChartBallPath on the set where the affine z stays in the chart target. Composition of Continuous affine + ContinuousOn chart inverse.

lemma ChartBallPath_continuousOn_target_set {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (anchor P Q : X) (S : Set ℝ)
    (h_target : ∀ t ∈ S,
      ((1 - (t : ℂ)) * (chartAt ℂ anchor) P + (t : ℂ) * (chartAt ℂ anchor) Q)
        ∈ (chartAt ℂ anchor).target) :
    ContinuousOn (ChartBallPath anchor P Q) S

chartAt_symm_contMDiffOn

The chart-coordinate inverse (chartAt ℂ P).symm is ContMDiffOn on the chart target — Mathlib's contMDiffOn_chart_symm.

lemma chartAt_symm_contMDiffOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (P : X) :
    ContMDiffOn 𝓘(ℂ) 𝓘(ℂ) ω
      (fun z : ℂ => (chartAt ℂ P).symm z) (chartAt ℂ P).target