Theorem: sum_Ks (Carleson/Carleson.lean)

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
⊢ ∑ i ∈ s, Ks K D ψ i x y = K x y
Tactic:
have h2 : 0 < dist x y := dist_pos.mpr h
State after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ ∑ i ∈ s, Ks K D ψ i x y = K x y

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ ∑ i ∈ s, Ks K D ψ i x y = K x y
Tactic:
simp_rw [Ks, ← Finset.mul_sum]
State after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ K x y * ∑ i ∈ s, ↑(ψ (D ^ i * dist x y)) = K x y

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ K x y * ∑ i ∈ s, ↑(ψ (D ^ i * dist x y)) = K x y
Tactic:
norm_cast
State after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ K x y * ↑(∑ i ∈ s, ψ (D ^ i * dist x y)) = K x y

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ K x y * ↑(∑ i ∈ s, ψ (D ^ i * dist x y)) = K x y
Tactic:
suffices ∑ i in s, ψ (D ^ i * dist x y) = 1 by
  simp [this]
State after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ ∑ i ∈ s, ψ (D ^ i * dist x y) = 1

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ ∑ i ∈ s, ψ (D ^ i * dist x y) = 1
Tactic:
rw [← Finset.sum_subset hs, h3ψ _ h2]
State after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ ∀ x_1 ∈ s, x_1 ∉ nonzeroS D (dist x y) → ψ (D ^ x_1 * dist x y) = 0

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
⊢ ∀ x_1 ∈ s, x_1 ∉ nonzeroS D (dist x y) → ψ (D ^ x_1 * dist x y) = 0
Tactic:
intros
State after:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
x✝ : ℤ
a✝¹ : x✝ ∈ s
a✝ : x✝ ∉ nonzeroS D (dist x y)
⊢ ψ (D ^ x✝ * dist x y) = 0

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
x✝ : ℤ
a✝¹ : x✝ ∈ s
a✝ : x✝ ∉ nonzeroS D (dist x y)
⊢ ψ (D ^ x✝ * dist x y) = 0
Tactic:
rwa [psi_eq_zero_iff h2ψ h2 hD]
State after:
no goals

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s✝ : ℤ
x y : X
hD✝ : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
s : Finset ℤ
hs : nonzeroS D (dist x y) ⊆ s
hD : 1 < D
h : x ≠ y
h2 : 0 < dist x y
this : ∑ i ∈ s, ψ (D ^ i * dist x y) = 1
⊢ K x y * ↑(∑ i ∈ s, ψ (D ^ i * dist x y)) = K x y
Tactic:
simp [this]
State after:
no goals