import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Normed.Module.BasicSmooth dyadic weights
The analytic sums in this project are localized by smooth functions supported
on [1/2, 1]. Keeping the support interval fixed makes the scale parameter
visible in the argument of the weight: W (x / X) localizes x to
[X/2, X].
namespace ElevenTwelfthsopen Setopen scoped ContDiff
A smooth function supported on the standard dyadic interval [1/2, 1].
@[ext]
structure SmoothDyadicWeight (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] where
toFun : ℝ → E
contDiff : ContDiff ℝ ∞ toFun
support_subset : Function.support toFun ⊆ Icc (1 / 2) 1namespace SmoothDyadicWeightvariable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]instance : CoeFun (SmoothDyadicWeight E) fun _ ↦ ℝ → E :=
⟨SmoothDyadicWeight.toFun⟩
A dyadic weight vanishes away from [1/2, 1].
theorem eq_zero_of_not_mem (W : SmoothDyadicWeight E) {x : ℝ}
(hx : x ∉ Icc (1 / 2 : ℝ) 1) :
W x = 0 := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:x ∉ Icc (1 / 2) 1⊢ W.toFun x = 0
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:x ∉ Icc (1 / 2) 1hne:¬W.toFun x = 0⊢ False
All goals completed! 🐙theorem eq_zero_of_lt_half (W : SmoothDyadicWeight E) {x : ℝ} (hx : x < 1 / 2) : W x = 0 := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:x < 1 / 2⊢ W.toFun x = 0
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:x < 1 / 2⊢ x ∉ Icc (1 / 2) 1
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:x < 1 / 2⊢ ¬1 / 2 ≤ x ∨ ¬x ≤ 1
All goals completed! 🐙theorem eq_zero_of_one_lt (W : SmoothDyadicWeight E) {x : ℝ} (hx : 1 < x) : W x = 0 := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:1 < x⊢ W.toFun x = 0
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:1 < x⊢ x ∉ Icc (1 / 2) 1
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EW:SmoothDyadicWeight Ex:ℝhx:1 < x⊢ ¬1 / 2 ≤ x ∨ ¬x ≤ 1
All goals completed! 🐙end SmoothDyadicWeightA real smooth dyadic weight suitable for weighting a mean square.
@[ext]
structure SmoothDyadicCutoff extends SmoothDyadicWeight ℝ where
nonnegative : ∀ x, 0 ≤ toFun xnamespace SmoothDyadicCutoffinstance : CoeFun SmoothDyadicCutoff fun _ ↦ ℝ → ℝ :=
⟨fun V ↦ V.toFun⟩theorem apply_nonnegative (V : SmoothDyadicCutoff) (x : ℝ) : 0 ≤ V x :=
V.nonnegative xend SmoothDyadicCutoffend ElevenTwelfths