Smooth cutoff functions for operator-core arguments

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Generator
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Multiplier
import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

noncomputable section
open MeasureTheory Filter Topology Metric Set InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy Energy.WeightedGradient
section Cutoff
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
/-- One fixed smooth profile, equal to one on the ball of radius five and supported in the ball
of radius eight. -/
 def profile : ContDiffBump (0 : V) := ⟨5, 8, by norm_num, by norm_num⟩
/-- The scaled cutoff `χ_r (y) = profile (r⁻¹ • y)`: one on `closedBall 0 (5 r)`, zero off
`ball 0 (8 r)`, with gradient of size `O(1/r)`. -/
 def cutoff (r : ℝ) (y : V) : ℝ := (FunctionalInequalities.KLS.LogConcave.profile (V := V)) (r⁻¹ • y)
 theorem contDiff_cutoff (r : ℝ) : ContDiff ℝ ∞ (FunctionalInequalities.KLS.LogConcave.cutoff (V := V) r) :=
  (FunctionalInequalities.KLS.LogConcave.profile (V := V)).contDiff.comp (contDiff_id.const_smul _)
 theorem cutoff_eq_zero {r : ℝ} (hr : 0 < r) {y : V} (hy : 8 * r ≤ ‖y‖) :
    FunctionalInequalities.KLS.LogConcave.cutoff (V := V) r y = 0 := by
  apply (FunctionalInequalities.KLS.LogConcave.profile (V := V)).zero_of_le_dist
  rw [dist_zero_right, norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hr),
    ← div_eq_inv_mul, le_div_iff₀ hr]
  exact hy
 theorem tsupport_cutoff_subset {r : ℝ} (hr : 0 < r) :
    tsupport (FunctionalInequalities.KLS.LogConcave.cutoff (V := V) r) ⊆ closedBall (0 : V) (8 * r) := by
  refine closure_minimal (fun y hy => ?_) isClosed_closedBall
  rw [mem_closedBall, dist_zero_right]
  by_contra h
  exact hy (FunctionalInequalities.KLS.LogConcave.cutoff_eq_zero hr (le_of_lt (not_le.1 h)))
 theorem hasCompactSupport_cutoff {r : ℝ} (hr : 0 < r) :
    HasCompactSupport (FunctionalInequalities.KLS.LogConcave.cutoff (V := V) r) :=
  HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall (0 : V) (8 * r))
    ((subset_tsupport _).trans (FunctionalInequalities.KLS.LogConcave.tsupport_cutoff_subset hr))
end Cutoff
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
end LogConcave
end KLS
end FunctionalInequalities