diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 61d74494..6f28692d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -6,9 +6,24 @@ Simply make a pull request with a change. Some remarks: * Some statements will be missing hypotheses. Don't hesitate adding hypotheses to a result, especially if it is already assumed elsewhere. Assuming that functions are measurable is always fine. +* Some estimates about norms or `ENNReal.toReal` will need a separate statement that the value is (almost everywhere) finite. * Many inequalities are up to some constant factor (depending on `a` and `q`). We put these constants in a separate def, so that the proofs hopefully break slighlty less easily. Feel free to improve these constants: - either just write a comment in the Lean file that the constant can be improved to X - or improve the constant in Lean with a comment that this has to be incorporated in the blueprint - or improve the constant both in Lean and the TeX file, making sure you also fix all downstream uses of the lemma. +* Feel free to change definitions/theorem statements to more convenient versions. Especially when deciding to put (in)equalities in `ℝ≥0∞`, `ℝ≥0` or `ℝ`, it is hard to know what is most convenient in advance. +* With suprema, it's probably most convenient to take suprema over `ℝ≥0∞`, and potentially apply `ENNReal.toReal` afterwards. + +Below, I will try to give a translation of some notation/conventions. + +| Blueprint | Lean | Remarks | +| --------- | ---------- | ------- | +| `⊂` | `⊆` | | +| `𝔓(𝔓')` | `lowerClosure 𝔓'` | | +| `λp ≲ λ'p'` | `smul l p ≤ smul l' p' ` | | +| `p ≲ p'` | `smul 1 p ≤ smul 1 p' ` | Beware that this is not the same as `p ≤ p'`. | +| `d_B(f,g)` | `dist_{x, r} f g` | Assuming `B = B(x,r)` is the ball with center `x` and radius `r`. Lean also has the variants `nndist_` and `ball_`. | +| `d_{Iᵒ}(f,g)` | `dist_{I} f g` | | +| `d_{𝔭}(f,g)` | `dist_(𝔭) f g` | `d_{𝔭}(f,g) = d_{𝓘(p)ᵒ}(f,g)`. | diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index b0cca6b5..ea53c486 100644 --- a/Carleson/Defs.lean +++ b/Carleson/Defs.lean @@ -329,3 +329,33 @@ scoped notation "o" => cancelPt X scoped notation "S" => S X end ShortVariables + +open scoped ShortVariables +variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} + [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] + +/-- the L^∞-normalized τ-Hölder norm. Do we use this for other values of τ? -/ +@[nolint unusedArguments] +def hnorm [ProofData a q K σ₁ σ₂ F G] (ϕ : X → ℂ) (x₀ : X) (R : ℝ≥0) : ℝ≥0∞ := + ⨆ (x ∈ ball x₀ R), (‖ϕ x‖₊ : ℝ≥0∞) + + R ^ τ * ⨆ (x ∈ ball x₀ R) (y ∈ ball x₀ R) (_ : x ≠ y), (‖ϕ x - ϕ y‖₊ / (nndist x y) ^ τ : ℝ≥0∞) + +/-! Lemma 2.1.1 -/ + +-- Note: See also/prove card_le_of_le_dist in DoublingMeasure. +lemma mk_le_of_le_dist {x₀ : X} {r R : ℝ} (hr : 0 < r) {f : Θ X} {k : ℕ} + {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k)) + (h2𝓩 : ∀ z z', z ∈ 𝓩 → z' ∈ 𝓩 → z ≠ z' → r ≤ dist_{x₀, R} z z') : + Cardinal.mk 𝓩 ≤ 2 ^ (k * ⌊a⌋₊) := sorry + +-- the following two lemma should follow easily from `mk_le_of_le_dist`. + +lemma card_le_of_le_dist' {x₀ : X} {r R : ℝ} (hr : 0 < r) {f : Θ X} {k : ℕ} + {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k)) + (h2𝓩 : ∀ z z', z ∈ 𝓩 → z' ∈ 𝓩 → z ≠ z' → r ≤ dist_{x₀, R} z z') : + Nat.card 𝓩 ≤ 2 ^ (k * ⌊a⌋₊) := sorry + +lemma finite_of_le_dist {x₀ : X} {r R : ℝ} (hr : 0 < r) {f : Θ X} {k : ℕ} + {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k)) + (h2𝓩 : ∀ z z', z ∈ 𝓩 → z' ∈ 𝓩 → z ≠ z' → r ≤ dist_{x₀, R} z z') : + 𝓩.Finite := sorry diff --git a/Carleson/DoublingMeasure.lean b/Carleson/DoublingMeasure.lean index d9c5ac5a..06231f02 100644 --- a/Carleson/DoublingMeasure.lean +++ b/Carleson/DoublingMeasure.lean @@ -1,5 +1,5 @@ import Carleson.CoverByBalls -import Carleson.ToMathlib.MeasureReal +import Carleson.ToMathlib.Misc import Mathlib.Analysis.NormedSpace.FiniteDimension import Mathlib.Analysis.SpecialFunctions.Log.Base import Mathlib.MeasureTheory.Integral.Average diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index 3c2574f8..c7c2e042 100644 --- a/Carleson/GridStructure.lean +++ b/Carleson/GridStructure.lean @@ -52,11 +52,13 @@ attribute [coe] GridStructure.coe𝓓 instance : Coe (𝓓 X) (Set X) := ⟨GridStructure.coe𝓓⟩ instance : Membership X (𝓓 X) := ⟨fun x i ↦ x ∈ (i : Set X)⟩ instance : HasSubset (𝓓 X) := ⟨fun i j ↦ (i : Set X) ⊆ (j : Set X)⟩ +instance : HasSSubset (𝓓 X) := ⟨fun i j ↦ (i : Set X) ⊂ (j : Set X)⟩ /- not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas -/ @[simp] lemma 𝓓.mem_def {x : X} {i : 𝓓 X} : x ∈ i ↔ x ∈ (i : Set X) := .rfl @[simp] lemma 𝓓.subset_def {i j : 𝓓 X} : i ⊆ j ↔ (i : Set X) ⊆ (j : Set X) := .rfl +@[simp] lemma 𝓓.ssubset_def {i j : 𝓓 X} : i ⊂ j ↔ (i : Set X) ⊂ (j : Set X) := .rfl def s : 𝓓 X → ℤ := GridStructure.s def c : 𝓓 X → X := GridStructure.c @@ -104,7 +106,6 @@ def 𝔠 (p : 𝔓 X) : X := c (𝓘 p) def 𝔰 (p : 𝔓 X) : ℤ := s (𝓘 p) end -local notation "dist_(" D "," 𝔭 ")" => @dist (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _ local notation "ball_(" D "," 𝔭 ")" => @ball (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _ /-- A tile structure. -/ @@ -126,11 +127,31 @@ open scoped ShortVariables variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o] +notation "dist_{" I "}" => @dist (WithFunctionDistance (c I) (D ^ s I / 4)) _ +notation "nndist_{" I "}" => @nndist (WithFunctionDistance (c I) (D ^ s I / 4)) _ +notation "ball_{" I "}" => @ball (WithFunctionDistance (c I) (D ^ s I / 4)) _ +-- maybe we should delete the following three notations, and just use the previous three? notation "dist_(" 𝔭 ")" => @dist (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _ +notation "nndist_(" 𝔭 ")" => @nndist (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _ notation "ball_(" 𝔭 ")" => @ball (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _ +@[simp] lemma dist_𝓘 (p : 𝔓 X) {f g : Θ X} : dist_{𝓘 p} f g = dist_(p) f g := rfl +@[simp] lemma nndist_𝓘 (p : 𝔓 X) {f g : Θ X} : nndist_{𝓘 p} f g = nndist_(p) f g := rfl +@[simp] lemma ball_𝓘 (p : 𝔓 X) {f : Θ X} {r : ℝ} : ball_{𝓘 p} f r = ball_(p) f r := rfl -/- The set `E` defined in Proposition 2.0.2. -/ +/-- Lemma 2.1.2, part 1. -/ +lemma 𝓓.dist_mono {I J : 𝓓 X} (hpq : I ⊆ J) {f g : Θ X} : + dist_{I} f g ≤ dist_{J} f g := by + sorry + +def C2_1_2 (a : ℝ) : ℝ := 2 ^ (-95 * a) + +/-- Lemma 2.1.2, part 2. -/ +lemma 𝓓.dist_strictMono {I J : 𝓓 X} (hpq : I ⊂ J) {f g : Θ X} : + dist_{I} f g ≤ C2_1_2 a * dist_{J} f g := by + sorry + +/-- The set `E` defined in Proposition 2.0.2. -/ def E (p : 𝔓 X) : Set X := { x ∈ 𝓘 p | Q x ∈ Ω p ∧ 𝔰 p ∈ Icc (σ₁ x) (σ₂ x) } @@ -138,27 +159,13 @@ section T variable {p : 𝔓 X} {f : X → ℂ} {q : ℝ≥0∞} -/- The operator `T_𝔭` defined in Proposition 2.0.2, considered on the set `F`. +/-- The operator `T_𝔭` defined in Proposition 2.0.2, considered on the set `F`. It is the map `T ∘ (1_F * ·) : f ↦ T (1_F * f)`, also denoted `T1_F` The operator `T` in Proposition 2.0.2 is therefore `applied to `(F := Set.univ)`. -/ def T (p : 𝔓 X) (f : X → ℂ) : X → ℂ := indicator (E p) fun x ↦ ∫ y, exp (Q x x - Q x y) * K x y * ψ (D ^ (- 𝔰 p) * dist x y) * F.indicator f y --- lemma Memℒp_T (hf : Memℒp f q) : Memℒp (T p f) q := --- by sorry - --- /- The operator `T`, defined on `L^2` maps. -/ --- def T₂ (f : X →₂[volume] ℂ) : X →₂[volume] ℂ := --- Memℒp.toLp (T K σ₁ σ₂ ψ p F f) <| Memℒp_T K σ₁ σ₂ ψ p F <| Lp.memℒp f - --- /- The operator `T`, defined on `L^2` maps as a continuous linear map. -/ --- def TL : (X →₂[volume] ℂ) →L[ℂ] (X →₂[volume] ℂ) where --- toFun := T₂ K σ₁ σ₂ ψ p F --- map_add' := sorry --- map_smul' := sorry --- cont := by sorry - end T variable (X) in @@ -177,8 +184,8 @@ lemma toTileLike_injective : Injective (fun p : 𝔓 X ↦ toTileLike p) := sorr instance : PartialOrder (𝔓 X) := PartialOrder.lift toTileLike toTileLike_injective /-- This is not defined as such in the blueprint, but `λp ≲ λ'p'` can be written using - `smul λ p ≤ smul λ' p'`. - Beware: `smul 1 p` is very different from `toTileLike p`! -/ +`smul l p ≤ smul l' p'`. +Beware: `smul 1 p` is very different from `toTileLike p`. -/ def smul (l : ℝ) (p : 𝔓 X) : TileLike X := (𝓘 p, ball_(p) (𝒬 p) l) @@ -204,12 +211,6 @@ def dens₂ (𝔓' : Set (𝔓 X)) : ℝ≥0∞ := ⨆ (p ∈ 𝔓') (r ≥ 4 * D ^ 𝔰 p), volume (F ∩ ball (𝔠 p) r) / volume (ball (𝔠 p) r) -/-- the L^∞-normalized τ-Hölder norm. Do we use this for other values of τ? -/ -@[nolint unusedArguments] -def hnorm [ProofData a q K σ₁ σ₂ F G] (ϕ : X → ℂ) (x₀ : X) (R : ℝ≥0) : ℝ≥0∞ := - ⨆ (x ∈ ball x₀ R), (‖ϕ x‖₊ : ℝ≥0∞) + - R ^ τ * ⨆ (x ∈ ball x₀ R) (y ∈ ball x₀ R) (_ : x ≠ y), (‖ϕ x - ϕ y‖₊ / (nndist x y) ^ τ : ℝ≥0∞) - -- a small characterization that might be useful lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) : IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄) ↔ @@ -229,14 +230,6 @@ instance : CoeTC (Tree X) (Set (𝔓 X)) where coe p := ((p : Finset (𝔓 X)) : instance : Membership (𝔓 X) (Tree X) := ⟨fun x p => x ∈ (p : Set _)⟩ instance : Preorder (Tree X) := Preorder.lift Tree.carrier --- LaTeX note: $D ^ {s(p)}$ should be $D ^ {s(I(p))}$ --- class Tree.IsThin (𝔗 : Tree X) : Prop where --- thin {p : 𝔓 X} (hp : p ∈ 𝔗) : ball (𝔠 p) (8 * a/-fix-/ * D ^ 𝔰 p) ⊆ 𝓓 (𝓘 𝔗.top) - --- alias Tree.thin := Tree.IsThin.thin - --- def Δ (p : 𝔓 X) (Q' : C(X, ℝ)) : ℝ := localOscillation (𝓓 (𝓘 p)) (𝒬 p) Q' + 1 - variable (X) in /-- An `n`-forest -/ structure Forest (n : ℕ) where @@ -260,7 +253,14 @@ end TileStructure --below is old -namespace Forest +-- class Tree.IsThin (𝔗 : Tree X) : Prop where +-- thin {p : 𝔓 X} (hp : p ∈ 𝔗) : ball (𝔠 p) (8 * a/-fix-/ * D ^ 𝔰 p) ⊆ 𝓓 (𝓘 𝔗.top) + +-- alias Tree.thin := Tree.IsThin.thin + +-- def Δ (p : 𝔓 X) (Q' : C(X, ℝ)) : ℝ := localOscillation (𝓓 (𝓘 p)) (𝒬 p) Q' + 1 + +-- namespace Forest /- Do we want to treat a forest as a set of trees, or a set of elements from `𝔓 X`? -/ @@ -278,19 +278,13 @@ namespace Forest -- /-- The union of all the trees in the forest. -/ -- def carrier (𝔉 : Forest G Q δ n) : Set (𝔓 X) := ⋃ 𝔗 ∈ 𝔉.I, 𝔗 -end Forest +-- end Forest -/-- Hardy-Littlewood maximal function -/ -def maximalFunction {X E} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup E] - (μ : Measure X) (f : X → E) (x : X) : ℝ := - ⨆ (x' : X) (δ : ℝ) (_hx : x ∈ ball x' δ), - ⨍⁻ y, ‖f y‖₊ ∂μ.restrict (ball x' δ) |>.toReal +-- def boundedTiles (F : Set X) (t : ℝ) : Set (𝔓 X) := +-- { p : 𝔓 X | ∃ x ∈ 𝓘 p, maximalFunction volume (Set.indicator F (1 : X → ℂ)) x ≤ t } -def boundedTiles (F : Set X) (t : ℝ) : Set (𝔓 X) := - { p : 𝔓 X | ∃ x ∈ 𝓘 p, maximalFunction volume (Set.indicator F (1 : X → ℂ)) x ≤ t } - -set_option linter.unusedVariables false in -variable (X) in -class SmallBoundaryProperty (η : ℝ) : Prop where - volume_diff_le : ∃ (C : ℝ) (hC : C > 0), ∀ (x : X) r (δ : ℝ), 0 < r → 0 < δ → δ < 1 → - volume.real (ball x ((1 + δ) * r) \ ball x ((1 - δ) * r)) ≤ C * δ ^ η * volume.real (ball x r) +-- set_option linter.unusedVariables false in +-- variable (X) in +-- class SmallBoundaryProperty (η : ℝ) : Prop where +-- volume_diff_le : ∃ (C : ℝ) (hC : C > 0), ∀ (x : X) r (δ : ℝ), 0 < r → 0 < δ → δ < 1 → +-- volume.real (ball x ((1 + δ) * r) \ ball x ((1 - δ) * r)) ≤ C * δ ^ η * volume.real (ball x r) diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean index 72d623bf..8398007a 100644 --- a/Carleson/Psi.lean +++ b/Carleson/Psi.lean @@ -15,7 +15,6 @@ def ψ (D x : ℝ) : ℝ := set_option hygiene false scoped[ShortVariables] notation "ψ" => ψ (defaultD a) - lemma support_ψ : support (ψ D) = Ioo (4 * D)⁻¹ 2⁻¹ := sorry lemma lipschitzWith_ψ (D : ℝ≥0) : LipschitzWith (4 * D) (ψ D) := sorry lemma finsum_ψ : ∑ᶠ s : ℤ, ψ D (D ^ s * x) = 1 := sorry @@ -26,13 +25,6 @@ variable (D) in def nonzeroS (x : ℝ) : Finset ℤ := lemma sum_ψ : ∑ s in nonzeroS D x, ψ D (D ^ s * x) = 1 := sorry --- move -theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by - rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right] - -theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ z - 1 < c := by - rw_mod_cast [← Int.add_one_le_ceil_iff, sub_add_cancel] - lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) (hD : 1 < D) : i ∈ nonzeroS D x ↔ (D ^ i * x) ∈ Ioo (4 * D)⁻¹ 2⁻¹ := by rw [Set.mem_Ioo, nonzeroS, Finset.mem_Icc] @@ -74,6 +66,26 @@ lemma sum_Ks {t : Finset ℤ} (hs : nonzeroS D (dist x y) ⊆ t) (hD : 1 < D) (h intros rwa [psi_eq_zero_iff h hD] -lemma sum_Ks' {s : Finset ℤ} - (hs : ∀ i : ℤ, (D ^ i * dist x y) ∈ Ioo (4 * D)⁻¹ 2⁻¹ → i ∈ s) - (hD : 1 < D) (h : x ≠ y) : ∑ i in s, Ks i x y = K x y := sorry +-- maybe this version is also useful? +-- lemma sum_Ks' {t : Finset ℤ} +-- (hs : ∀ i : ℤ, (D ^ i * dist x y) ∈ Ioo (4 * D)⁻¹ 2⁻¹ → i ∈ t) +-- (hD : 1 < D) (h : x ≠ y) : ∑ i in t, Ks i x y = K x y := by +-- sorry + +lemma dist_mem_Icc_of_Ks_ne_zero {s : ℤ} (hs : s ∈ Icc (-S) S) {x y : X} + (h : Ks s x y ≠ 0) : dist x y ∈ Icc (D ^ (s - 1) / 4) (D ^ s / 2) := by + sorry + +/-- The constant appearing in part 2 of Lemma 2.1.3. -/ +def C2_1_3 (a : ℝ) : ℝ := 2 ^ (102 * a ^ 3) +/-- The constant appearing in part 3 of Lemma 2.1.3. -/ +def D2_1_3 (a : ℝ) : ℝ := 2 ^ (150 * a ^ 3) + +lemma norm_Ks_le {s : ℤ} (hs : s ∈ Icc (-S) S) {x y : X} : + ‖Ks s x y‖ ≤ C2_1_3 a / volume.real (ball x (D ^ s)) := by + sorry + +lemma norm_Ks_sub_Ks_le {s : ℤ} (hs : s ∈ Icc (-S) S) {x y y' : X} : + ‖Ks s x y - Ks s x y'‖ ≤ + D2_1_3 a / volume.real (ball x (D ^ s)) * (dist y y' / D ^ s) ^ a⁻¹ := by + sorry diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 8f2b53e0..2f242ad3 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -2,5 +2,19 @@ import Mathlib.Analysis.Convex.PartitionOfUnity import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.MeasureTheory.Integral.Bochner import Mathlib.Topology.MetricSpace.Holder +import Carleson.ToMathlib.MeasureReal + +/- +* This file can import all ToMathlib files. +* If adding more than a few result, please put them in a more appropriate file in ToMathlib. +-/ attribute [gcongr] Metric.ball_subset_ball + + +-- move +theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by + rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right] + +theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ z - 1 < c := by + rw_mod_cast [← Int.add_one_le_ceil_iff, sub_add_cancel] diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 80b3532a..72ff73d1 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -559,7 +559,7 @@ \chapter{Proof of Metric Space Carleson, overview} (1 + d_{B}(\mfa,\mfb))^{-\frac{1}{2a^2+a^3}} \,. \end{equation} - \end{proposition} +\end{proposition} We further formulate a classical Vitali covering result and maximal function estimate that we need throughout several sections. @@ -574,6 +574,9 @@ \chapter{Proof of Metric Space Carleson, overview} \begin{proposition}[Hardy--Littlewood] \label{Hardy-Littlewood} +\leanok +\lean{measure_biUnion_le_lintegral, maximalFunction_lt_top, snorm_maximalFunction, M_lt_top, + laverage_le_M, snorm_M_le} \uses{layer-cake-representation,covering-separable-space} Let $\mathcal{B}$ be a finite collection of balls in $X$. If for some $\lambda>0$ and some measurable function $u:X\to [0,\infty)$ we have @@ -613,6 +616,8 @@ \section{Auxiliary lemmas} \begin{lemma}[ball metric entropy] \label{ball-metric-entropy} + \leanok + \lean{mk_le_of_le_dist} Let $B' \subset X$ be a ball. Let $r > 0$, $\mfa \in \Mf$ and $k \in \mathbb{N}$. Suppose that $\mathcal{Z} \subset B_{B'}(\mfa, r2^k)$ satisfies that for all $z, z' \in \mathcal{Z}$ with $z \ne z'$, we have $d_{B'}(z,z') \ge r$. Then $$ |\mathcal{Z}| \le 2^{ka}\,. @@ -631,6 +636,8 @@ \section{Auxiliary lemmas} \begin{lemma}[monotone cube metrics] \label{monotone-cube-metrics} + \leanok + \lean{𝓓.dist_mono, 𝓓.dist_strictMono} Let $(\mathcal{D}, c, s)$ be a grid structure. Denote for cubes $I \in \mathcal{D}$ $$ I^\circ := B(c(I), \frac{1}{4} D^{s(I)})\,. @@ -675,6 +682,8 @@ \section{Auxiliary lemmas} \begin{lemma}[kernel summand] \label{kernel-summand} +\leanok +\lean{dist_mem_Icc_of_Ks_ne_zero, norm_Ks_le, norm_Ks_sub_Ks_le} Let $-S\le s\le S$ and $x,y,y'\in X$. If $K_s(x,y)\neq 0$, then we have \begin{equation}\label{supp-Ks}