internlm/Lean-Github huggingface dataset:
Theorem: mem_nonzeroS_iff
Proof 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
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ 0 < (2 * x)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: mem_nonzeroS_iff
Proof 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
i : ℤ
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ 0 < (4 * x)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: psi_ne_zero_iff
Proof 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
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ ψ (D ^ s * x) ≠ 0 ↔ s ∈ nonzeroS D x
Tactic:
rw [← mem_support, h2ψ, mem_nonzeroS_iff hx hD]
Proof state after:
no goals
Theorem: psi_eq_zero_iff
Proof 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
x : ℝ
hx : 0 < x
hD : 1 < D
⊢ ψ (D ^ s * x) = 0 ↔ s ∉ nonzeroS D x
Tactic:
rw [← iff_not_comm, ← psi_ne_zero_iff h2ψ hx hD]
Proof state after:
no goals
Theorem: sum_Ks
Proof 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
Proof 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
Theorem: sum_Ks
Proof 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]
Proof 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
Theorem: sum_Ks
Proof 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
Proof 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
Theorem: sum_Ks
Proof 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]
Proof 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
Theorem: sum_Ks
Proof 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]
Proof 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
Theorem: sum_Ks
Proof 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
Proof 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
Theorem: sum_Ks
Proof 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]
Proof state after:
no goals
Theorem: sum_Ks
Proof 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]
Proof state after:
no goals
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
⊢ let rhs :=
    Ce3_1 a τ q * maximalFunction f x +
      ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖;
  CarlesonOperator K Θ f x ≤ rhs
Tactic:
intro rhs
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
⊢ CarlesonOperator K Θ f x ≤ rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
⊢ CarlesonOperator K Θ f x ≤ rhs
Tactic:
have h_rhs : 0 ≤ rhs := by
  sorry
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
⊢ CarlesonOperator K Θ f x ≤ rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
⊢ CarlesonOperator K Θ f x ≤ rhs
Tactic:
rw [CarlesonOperator]
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
⊢ ⨆ Q ∈ Θ, ⨆ R₁, ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
⊢ ⨆ Q ∈ Θ, ⨆ R₁, ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
refine Real.iSup_le (fun Q ↦ ?_) h_rhs
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
⊢ ⨆ (_ : Q ∈ Θ), ⨆ R₁, ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * cexp (I * Q y)‖ ≤
    rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
⊢ ⨆ (_ : Q ∈ Θ), ⨆ R₁, ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * cexp (I * Q y)‖ ≤
    rhs
Tactic:
refine Real.iSup_le (fun hQ ↦ ?_) h_rhs
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
⊢ ⨆ R₁, ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
⊢ ⨆ R₁, ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
refine Real.iSup_le (fun r ↦ ?_) h_rhs
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
r : ℝ
⊢ ⨆ R₂, ⨆ (_ : r < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo r R₂}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
r : ℝ
⊢ ⨆ R₂, ⨆ (_ : r < R₂), ‖∫ (y : X) in {y | dist x y ∈ Ioo r R₂}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
refine Real.iSup_le (fun R ↦ ?_) h_rhs
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
r R : ℝ
⊢ ⨆ (_ : r < R), ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Theorem: equation3_1
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
r R : ℝ
⊢ ⨆ (_ : r < R), ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
refine Real.iSup_le (fun hrR ↦ ?_) h_rhs
Proof 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
f : X → ℂ
hf : LocallyIntegrable f volume
hΘ : ∀ Q ∈ Θ, ∀ (x : X), (Q x).im = 0
rhs : ℝ :=
  Ce3_1 a τ q * maximalFunction f x +
    ⨆ Q ∈ Θ, ⨆ σ, ⨆ σ', ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖
h_rhs : 0 ≤ rhs
Q : C(X, ℂ)
hQ : Q ∈ Θ
r R : ℝ
hrR : r < R
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs