Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

One constant controls every positive-radius first derivative

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_fderiv_bound · theorem · Teaching coverage

Statement

For any real inner-product space E, there is a positive real constant C such that for every positive radius R and every point x∈E, the operator norm of the Fréchet derivative of χ_R at x is at most C/R. The constant is chosen before R and x from a global bound on the fixed scalar cutoff derivative.

\[\exists C>0\ \forall R>0\ \forall x\in E,\qquad\|D\chi_R(x)\|_{\mathrm{op}}\le\frac CR.\]

All objects and hypotheses

  • E is a normed additive commutative group with a real inner-product-space structure; no finite-dimensionality or completeness assumption.
  • C is existential and strictly positive; R>0 and x∈E are universally quantified after C.
  • The derivative is genuine here because χ_R is smooth for R>0; the Lean expression remains the totalized `fderiv`.

Mathematical proof

1. Fix the scalar derivative constant before choosing the radius

The scalar boundedness theorem supplies C>0 such that |q′(t)|≤C for every t. Keep this same C for all radii and points.

\[\exists C>0\ \forall t\in\mathbb R,\ |q'(t)|\le C.\]
Corresponding Lean step

obtain ⟨C, hC_pos, hC_bound⟩ := smoothUnitCutoff_deriv_bounded; refine ⟨C, hC_pos, ?_⟩; intro R hR x

2. The derivative vanishes strictly inside the plateau

If ‖x‖<R, the triangle inequality shows that χ_R agrees with one on a neighborhood of x of radius R−‖x‖. Its derivative is therefore the zero linear map, and the desired nonnegative upper bound follows.

\[\|x\|<R\ \Longrightarrow\ D\chi_R(x)=D(1)(x)=0,\qquad0\le C/R.\]
Corresponding Lean step

Metric.eventually_nhds_iff.mpr ⟨R - ‖x‖, hradius, ?_⟩; radialSmoothCutoff_eq_one_of_norm_le hR; (Filter.EventuallyEq.fderiv_eq h_eq).trans hconst; div_nonneg hC_pos.le hR.le

3. Use genuine differentiability for the chain rule outside the inner ball

If R≤‖x‖, then x≠0. The inner-product norm is differentiable there, so h(y)=‖y‖/R is differentiable at x; q is differentiable everywhere. The Fréchet chain rule therefore applies.

\[D\chi_R(x)=Dq(\|x\|/R)\circ Dh(x),\qquad h(y)=\|y\|/R.\]
Corresponding Lean step

(contDiffAt_norm ℝ hx_ne).differentiableAt WithTop.top_ne_zero; hnorm.mul_const R⁻¹; smoothUnitCutoff_contDiff.differentiable ...; fderiv_comp x hcutoff_diff hnorm_diff

4. Multiply the two operator-norm bounds

The norm of a composition is at most the product of the norms. The scalar derivative factor is at most C; the scaled-norm derivative factor is at most 1/R by the preceding Lipschitz-based lemma. Their product is C/R.

\[\|D\chi_R(x)\|_{\mathrm{op}}\le |q'(\|x\|/R)|\,\|Dh(x)\|_{\mathrm{op}}\le C(1/R)=C/R.\]
Corresponding Lean step

ContinuousLinearMap.opNorm_comp_le _ _; rw [← norm_deriv_eq_norm_fderiv]; exact hC_bound _; exact fderiv_norm_div_bound hR x; ... _ = C / R := by ring

Lean statement · radialSmoothCutoff_fderiv_bound

The existential statement does not give a numerical or optimal value of C. The proof uses only first-order ingredients and the scalar first-derivative bound; it neither invokes nor requires the later second-order API. The source's surrounding Radial section contributes the implicit type E and its NormedAddCommGroup instance; further structures appear explicitly in the declaration.

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.

theorem radialSmoothCutoff_fderiv_bound [InnerProductSpace ℝ E] :
    ∃ C : ℝ, 0 < C ∧ ∀ R : ℝ, 0 < R → ∀ x : E,
      ‖fderiv ℝ (radialSmoothCutoff R : E → ℝ) x‖ ≤ C / R

Exact module and namespace context

Lean proof · radialSmoothCutoff_fderiv_bound

Actual proof outline: Fix the scalar derivative constant before choosing the radius: Introducing R and x only after selecting C records the required scale-uniform quantifier order. The derivative vanishes strictly inside the plateau: The proof constructs actual neighborhood equality `h_eq`; it does not infer derivative equality from a single point value. Use genuine differentiability for the chain rule outside the inner ball: `fderiv_comp` is called with explicit differentiability witnesses for both factors. Totalization alone would not justify an unrestricted chain rule. Multiply the two operator-norm bounds: `norm_deriv_eq_norm_fderiv` identifies the norm of the scalar derivative with the operator norm of its one-dimensional Fréchet derivative.

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.

theorem radialSmoothCutoff_fderiv_bound [InnerProductSpace ℝ E] :
    ∃ C : ℝ, 0 < C ∧ ∀ R : ℝ, 0 < R → ∀ x : E,
      ‖fderiv ℝ (radialSmoothCutoff R : E → ℝ) x‖ ≤ C / R := by
  obtain ⟨C, hC_pos, hC_bound⟩ := smoothUnitCutoff_deriv_bounded
  refine ⟨C, hC_pos, ?_⟩
  intro R hR x
  by_cases hxR : ‖x‖ < R
  · have h_eq : ∀ᶠ y in 𝓝 x, radialSmoothCutoff R y = 1 := by
      have hradius : 0 < R - ‖x‖ := sub_pos.mpr hxR
      refine Metric.eventually_nhds_iff.mpr ⟨R - ‖x‖, hradius, ?_⟩
      intro y hy
      apply radialSmoothCutoff_eq_one_of_norm_le hR
      rw [dist_eq_norm] at hy
      have hynorm : ‖y‖ ≤ ‖x‖ + ‖y - x‖ := by
        calc
          ‖y‖ = ‖x + (y - x)‖ := by congr 1; abel
          _ ≤ ‖x‖ + ‖y - x‖ := norm_add_le x (y - x)
      linarith
    have hfderiv_eq : fderiv ℝ (radialSmoothCutoff R : E → ℝ) x = 0 := by
      have hconst : fderiv ℝ (fun _ : E => (1 : ℝ)) x = 0 := by simp
      exact (Filter.EventuallyEq.fderiv_eq h_eq).trans hconst
    rw [hfderiv_eq, norm_zero]
    exact div_nonneg hC_pos.le hR.le
  · push Not at hxR
    have hx_ne : x ≠ 0 := by
      intro hzero
      rw [hzero, norm_zero] at hxR
      linarith
    have hnorm_diff : DifferentiableAt ℝ (fun y : E => ‖y‖ / R) x := by
      have hnorm : DifferentiableAt ℝ (fun y : E => ‖y‖) x :=
        (contDiffAt_norm ℝ hx_ne).differentiableAt WithTop.top_ne_zero
      simpa only [div_eq_mul_inv] using hnorm.mul_const R⁻¹
    have hcutoff_diff : DifferentiableAt ℝ smoothUnitCutoff (‖x‖ / R) :=
      smoothUnitCutoff_contDiff.differentiable
        (WithTop.coe_ne_zero.mpr WithTop.top_ne_zero) (‖x‖ / R)
    have hchain :
        fderiv ℝ (radialSmoothCutoff R : E → ℝ) x =
          fderiv ℝ smoothUnitCutoff (‖x‖ / R) ∘L
            fderiv ℝ (fun y : E => ‖y‖ / R) x := by
      unfold radialSmoothCutoff
      exact fderiv_comp x hcutoff_diff hnorm_diff
    rw [hchain]
    calc
      ‖fderiv ℝ smoothUnitCutoff (‖x‖ / R) ∘L
          fderiv ℝ (fun y : E => ‖y‖ / R) x‖
          ≤ ‖fderiv ℝ smoothUnitCutoff (‖x‖ / R)‖ *
              ‖fderiv ℝ (fun y : E => ‖y‖ / R) x‖ :=
            ContinuousLinearMap.opNorm_comp_le _ _
      _ ≤ C * (1 / R) := by
        apply mul_le_mul
        · rw [← norm_deriv_eq_norm_fderiv]
          exact hC_bound _
        · exact fderiv_norm_div_bound hR x
        · exact norm_nonneg _
        · exact hC_pos.le
      _ = C / R := by ring

/-- The totalized derivative of the radial cutoff vanishes throughout the
outer zero region, including its boundary sphere.  At the boundary the cutoff
is a global minimum rather than locally constant; `IsLocalMin.fderiv_eq_zero`
records that distinction. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • This theorem is not a Hessian, Laplacian, or second-derivative estimate.
  • A fixed E is an ambient parameter; although the construction reuses the fixed scalar bound, the declaration does not quantify one C simultaneously over all space types.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • Metric.eventually_nhds_iff
  • Filter.EventuallyEq.fderiv_eq
  • contDiffAt_norm
  • DifferentiableAt.mul_const
  • fderiv_comp
  • ContinuousLinearMap.opNorm_comp_le
  • norm_deriv_eq_norm_fderiv

Mathematical sources

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