Coarse-graining support: Support.Sobolev.Foundations.Cutoff.Profile

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

One-dimensional smooth cutoff profiles

This file isolates the one-dimensional analytic input for quantitative cutoff constructions. The geometric ball and cube cutoffs should depend only on a profile carrying explicit first- and second-derivative bounds.

structure HCPolySupport.QuantitativeTransitionProfile : Type

A smooth transition profile with certified quantitative first and second derivative bounds.

The intended use is:

• θ t = 0 for t ≤ 0;
• θ t = 1 for 1 ≤ t;
• 0 ≤ θ ≤ 1;
• ‖θ'‖∞ ≤ derivBound;
• ‖θ''‖∞ ≤ secondDerivBound.

Keeping these constants in the profile avoids burying the hard one-dimensional analysis inside the ball and cube cutoff proofs.

• toFun : ℝ → ℝ

  The smooth transition function taking values in [0, 1], equal to zero on t ≤ 0 and one on t ≥ 1.

• smooth : ContDiff ℝ (↑⊤) self.toFun
• zero_of_nonpos {t : ℝ} : t ≤ 0 → self.toFun t = 0
• one_of_one_le {t : ℝ} : 1 ≤ t → self.toFun t = 1
• nonneg (t : ℝ) : 0 ≤ self.toFun t
• le_one (t : ℝ) : self.toFun t ≤ 1
• derivBound : ℝ

  A nonnegative uniform bound for the absolute value of the transition function's first derivative.

• derivBound_nonneg : 0 ≤ self.derivBound
• norm_deriv_le (t : ℝ) : ‖deriv self.toFun t‖ ≤ self.derivBound
• secondDerivBound : ℝ

  A nonnegative uniform bound for the absolute value of the transition function's second derivative.

• secondDerivBound_nonneg : 0 ≤ self.secondDerivBound
• norm_secondDeriv_le (t : ℝ) : ‖deriv (deriv self.toFun) t‖ ≤ self.secondDerivBound

@[instance_reducible]

instance HCPolySupport.QuantitativeTransitionProfile.instCoeFunForallReal : CoeFun QuantitativeTransitionProfile fun (x : QuantitativeTransitionProfile) => ℝ → ℝ

Equations

• HCPolySupport.QuantitativeTransitionProfile.instCoeFunForallReal = { coe := fun (θ : HCPolySupport.QuantitativeTransitionProfile) => θ.toFun }

noncomputable def HCPolySupport.smoothTransitionProfile (t : ℝ) : ℝ

The canonical smooth transition supplied by mathlib. This is the natural explicit formula to analyze: exp(-1/t) / (exp(-1/t) + exp(-1/(1-t))), with the endpoint extensions from Real.expNegInvGlue.

The basic shape facts are already in mathlib; the quantitative derivative bounds are the remaining one-dimensional project.

Equations

• HCPolySupport.smoothTransitionProfile t = t.smoothTransition

theorem HCPolySupport.smoothTransitionProfile.smooth : ContDiff ℝ (↑⊤) smoothTransitionProfile

theorem HCPolySupport.smoothTransitionProfile.zero_of_nonpos {t : ℝ} (ht : t ≤ 0) : smoothTransitionProfile t = 0

theorem HCPolySupport.smoothTransitionProfile.one_of_one_le {t : ℝ} (ht : 1 ≤ t) : smoothTransitionProfile t = 1

theorem HCPolySupport.smoothTransitionProfile.nonneg (t : ℝ) : 0 ≤ smoothTransitionProfile t

theorem HCPolySupport.smoothTransitionProfile.le_one (t : ℝ) : smoothTransitionProfile t ≤ 1

theorem HCPolySupport.smoothTransitionProfile.pos_of_pos {t : ℝ} (ht : 0 < t) : 0 < smoothTransitionProfile t

theorem HCPolySupport.smoothTransitionProfile.differentiable : Differentiable ℝ smoothTransitionProfile

theorem HCPolySupport.smoothTransitionProfile.deriv_zero_of_neg {t : ℝ} (ht : t < 0) : deriv smoothTransitionProfile t = 0

The derivative of the smooth transition vanishes on the open zero side.

theorem HCPolySupport.smoothTransitionProfile.deriv_zero_of_one_lt {t : ℝ} (ht : 1 < t) : deriv smoothTransitionProfile t = 0

The derivative of the smooth transition vanishes on the open one side.

theorem HCPolySupport.smoothTransitionProfile.continuous_deriv : Continuous (deriv smoothTransitionProfile)

theorem HCPolySupport.smoothTransitionProfile.deriv_zero_of_nonpos {t : ℝ} (ht : t ≤ 0) : deriv smoothTransitionProfile t = 0

The derivative of the smooth transition vanishes on the closed zero side.

The endpoint follows from continuity of the derivative and the open-side identity.

theorem HCPolySupport.smoothTransitionProfile.deriv_zero_of_one_le {t : ℝ} (ht : 1 ≤ t) : deriv smoothTransitionProfile t = 0

The derivative of the smooth transition vanishes on the closed one side.

The endpoint follows from continuity of the derivative and the open-side identity.

theorem HCPolySupport.smoothTransitionProfile.contDiff_deriv : ContDiff ℝ (↑⊤) (deriv smoothTransitionProfile)

theorem HCPolySupport.smoothTransitionProfile.continuous_secondDeriv : Continuous (deriv (deriv smoothTransitionProfile))

theorem HCPolySupport.smoothTransitionProfile.exists_deriv_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), ‖deriv smoothTransitionProfile t‖ ≤ C

theorem HCPolySupport.smoothTransitionProfile.exists_secondDeriv_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), ‖deriv (deriv smoothTransitionProfile) t‖ ≤ C

noncomputable def HCPolySupport.smoothTransitionProfile.derivBound : ℝ

Noncomputable global first-derivative bound for smoothTransitionProfile.

This is proved by compactness. It is intentionally separated from the later project of proving a small explicit numerical bound.

Equations

• HCPolySupport.smoothTransitionProfile.derivBound = HCPolySupport.smoothTransitionProfile.exists_deriv_bound.choose

theorem HCPolySupport.smoothTransitionProfile.derivBound_nonneg : 0 ≤ derivBound

theorem HCPolySupport.smoothTransitionProfile.norm_deriv_le (t : ℝ) : ‖deriv smoothTransitionProfile t‖ ≤ derivBound

noncomputable def HCPolySupport.smoothTransitionProfile.secondDerivBound : ℝ

Noncomputable global second-derivative bound for smoothTransitionProfile.

Equations

• HCPolySupport.smoothTransitionProfile.secondDerivBound = HCPolySupport.smoothTransitionProfile.exists_secondDeriv_bound.choose

theorem HCPolySupport.smoothTransitionProfile.secondDerivBound_nonneg : 0 ≤ secondDerivBound

theorem HCPolySupport.smoothTransitionProfile.norm_secondDeriv_le (t : ℝ) : ‖deriv (deriv smoothTransitionProfile) t‖ ≤ secondDerivBound

noncomputable def HCPolySupport.smoothTransitionProfile.quantitativeProfile : QuantitativeTransitionProfile

Real.smoothTransition packaged as a quantitative transition profile, with noncomputable compactness bounds for the first and second derivatives.

Equations

• One or more equations did not get rendered due to their size.