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 : ℝ
hrR : r < R
σ : ℤ := ⌊D.logb (2 * r)⌋ + 1
σ' : ℤ := ⌈D.logb (4 * R)⌉
h1 : ‖cexp (I * Q x)‖ = 1
⊢ ‖(∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)) -
        ∫ (a : X), (∑ i ∈ Finset.Icc σ σ', Ks K D ψ i x a) * f a * cexp (I * Q a)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

case hf
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
σ : ℤ := ⌊D.logb (2 * r)⌋ + 1
σ' : ℤ := ⌈D.logb (4 * R)⌉
h1 : ‖cexp (I * Q x)‖ = 1
⊢ ∀ i ∈ Finset.Icc σ σ', Integrable (fun a => Ks K D ψ i x a * f a * cexp (I * Q a)) volume

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
σ : ℤ := ⌊D.logb (2 * r)⌋ + 1
σ' : ℤ := ⌈D.logb (4 * R)⌉
⊢ Ce3_1 a τ q * maximalFunction f x +
      ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖ ≤
    rhs
Tactic:
have h3 :
  ∫ (y : X) in {y | dist x y ∈ Set.Ioo r R}, K x y * f y * cexp (I * Q y) =
    ∫ (y : X) in {y | dist x y ∈ Set.Ioo r R}, (∑ x_1 in Finset.Icc σ σ', Ks K D ψ x_1 x y) * f y * cexp (I * Q y) := 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
Q : C(X, ℂ)
hQ : Q ∈ Θ
r R : ℝ
hrR : r < R
σ : ℤ := ⌊D.logb (2 * r)⌋ + 1
σ' : ℤ := ⌈D.logb (4 * R)⌉
h1 : ‖cexp (I * Q x)‖ = 1
h3 :
  ∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y) =
    ∫ (y : X) in {y | dist x y ∈ Ioo r R}, (∑ x_1 ∈ Finset.Icc σ σ', Ks K D ψ x_1 x y) * f y * cexp (I * Q y)
⊢ ‖(∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)) -
        ∫ (a : X), (∑ i ∈ Finset.Icc σ σ', Ks K D ψ i x a) * f a * cexp (I * Q a)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

case hf
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
σ : ℤ := ⌊D.logb (2 * r)⌋ + 1
σ' : ℤ := ⌈D.logb (4 * R)⌉
h1 : ‖cexp (I * Q x)‖ = 1
⊢ ∀ i ∈ Finset.Icc σ σ', Integrable (fun a => Ks K D ψ i x a * f a * cexp (I * Q a)) volume

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
σ : ℤ := ⌊D.logb (2 * r)⌋ + 1
σ' : ℤ := ⌈D.logb (4 * R)⌉
⊢ Ce3_1 a τ q * maximalFunction f x +
      ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖ ≤
    rhs