Skip to content

Commit

Permalink
finish section 2
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Jun 20, 2024
1 parent 90571cc commit 08ff76b
Show file tree
Hide file tree
Showing 7 changed files with 135 additions and 61 deletions.
15 changes: 15 additions & 0 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)`. |
30 changes: 30 additions & 0 deletions Carleson/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion Carleson/DoublingMeasure.lean
Original file line number Diff line number Diff line change
@@ -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
Expand Down
90 changes: 42 additions & 48 deletions Carleson/GridStructure.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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. -/
Expand All @@ -126,39 +127,45 @@ 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) }

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
Expand All @@ -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)

Expand All @@ -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) '' 𝔄) ↔
Expand All @@ -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
Expand All @@ -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`? -/

Expand All @@ -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)
34 changes: 23 additions & 11 deletions Carleson/Psi.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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
14 changes: 14 additions & 0 deletions Carleson/ToMathlib/Misc.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
11 changes: 10 additions & 1 deletion blueprint/src/chapter/main.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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}\,.
Expand All @@ -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)})\,.
Expand Down Expand Up @@ -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}
Expand Down

0 comments on commit 08ff76b

Please sign in to comment.