An existing uniform second-derivative bound under dilation

Actual proof outline: Obtain continuity and compact support of the unit-radius second derivative: The code obtains its second-order input from the unit radial function itself. It does not call `smoothUnitCutoff_secondDeriv_bounded` or the first-order radial bound. Choose one positive global bound at unit radius: The names `C` and `C'` in Lean correspond to B and the positive C in the exposition. This choice precedes `intro R hR x`. Represent the radius change by a bounded linear dilation: `E →L[ℝ] E` is the type of real continuous linear maps. The positivity assumption removes the absolute value of R in the scaling norm. Express every cutoff as the unit cutoff after dilation: `funext` proves equality of functions by evaluating at an arbitrary point. This is an exact scaling identity, not an asymptotic approximation. Apply the exact second-derivative rule for a linear inner map: The actual helper is `ContinuousLinearMap.iteratedFDeriv_comp_right`; `compContinuousLinearMap (fun _ => L)` places the same linear map in both multilinear slots. Bound both linear slots and simplify the scale: The product indexed by `Fin 2` has exactly two factors. The final algebra is the displayed R⁻² scale.

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_iteratedFDeriv_two_bound
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] :
    ∃ C : ℝ, 0 < C ∧ ∀ R : ℝ, 0 < R → ∀ x : E,
      ‖iteratedFDeriv ℝ 2 (radialSmoothCutoff R : E → ℝ) x‖ ≤ C / R ^ 2 := by
  have hunit_smooth : ContDiff ℝ (⊤ : ℕ∞)
      (radialSmoothCutoff 1 : E → ℝ) :=
    radialSmoothCutoff_contDiff one_pos
  have hunit_continuous : Continuous
      (iteratedFDeriv ℝ 2 (radialSmoothCutoff 1 : E → ℝ)) :=
    hunit_smooth.continuous_iteratedFDeriv
      (WithTop.coe_le_coe.mpr (le_top : (2 : ℕ∞) ≤ ⊤))
  have hunit_support : HasCompactSupport
      (iteratedFDeriv ℝ 2 (radialSmoothCutoff 1 : E → ℝ)) :=
    (radialSmoothCutoff_hasCompactSupport one_pos).iteratedFDeriv 2
  obtain ⟨C, hC⟩ :=
    hunit_support.exists_bound_of_continuous hunit_continuous
  let C' : ℝ := max C 1
  have hC'_pos : 0 < C' := lt_max_of_lt_right one_pos
  refine ⟨C', hC'_pos, ?_⟩
  intro R hR x
  let L : E →L[ℝ] E := R⁻¹ • ContinuousLinearMap.id ℝ E
  have hL_norm : ‖L‖ ≤ 1 / R := by
    refine L.opNorm_le_bound (by positivity) ?_
    intro y
    simp only [L, smul_apply, ContinuousLinearMap.id_apply]
    rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hR]
    simp [one_div]
  have hfun : (radialSmoothCutoff R : E → ℝ) =
      (radialSmoothCutoff 1 : E → ℝ) ∘ L := by
    funext y
    simp only [radialSmoothCutoff, Function.comp_apply, L,
      smul_apply, ContinuousLinearMap.id_apply, div_one]
    rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hR]
    ring_nf
  rw [hfun]
  rw [L.iteratedFDeriv_comp_right hunit_smooth x
    (i := 2) (WithTop.coe_le_coe.mpr (le_top : (2 : ℕ∞) ≤ ⊤))]
  calc
    ‖(iteratedFDeriv ℝ 2 (radialSmoothCutoff 1 : E → ℝ) (L x)).compContinuousLinearMap
        (fun _ => L)‖ ≤
        ‖iteratedFDeriv ℝ 2 (radialSmoothCutoff 1 : E → ℝ) (L x)‖ *
          ∏ _ : Fin 2, ‖L‖ :=
      ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _
    _ = ‖iteratedFDeriv ℝ 2 (radialSmoothCutoff 1 : E → ℝ) (L x)‖ * ‖L‖ ^ 2 := by
      simp
    _ ≤ C' * (1 / R) ^ 2 := by
      gcongr
      exact (hC (L x)).trans (le_max_left C 1)
    _ = C' / R ^ 2 := by ring

/-- At each fixed point, the positive-scale radial cutoffs tend to one as the scale diverges. -/

Exact module and namespace context