Theorem: equation3_1 (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
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
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
let σ : ℤ := ⌊Real.logb D (2 * r)⌋ + 1
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
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs

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
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
let σ' : ℤ := ⌈Real.logb D (4 * R)⌉
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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs

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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤ rhs
Tactic:
trans Ce3_1 a τ q * maximalFunction f x +
  ‖∑ s in Finset.Icc σ σ', ∫ y, Ks K D ψ s x y * f y * exp (I * (Q y - Q x))‖
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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤
    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))‖

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

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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ ≤
    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))‖

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:
rw [← sub_le_iff_le_add]
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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ -
      ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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

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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ -
      ‖∑ s ∈ Finset.Icc σ σ', ∫ (y : X), Ks K D ψ s x y * f y * cexp (I * (Q y - Q x))‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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:
simp_rw [mul_sub, Complex.exp_sub, mul_div, integral_div, ← Finset.sum_div,
  norm_div]
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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ -
      ‖∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ / ‖cexp (I * Q x)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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

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)⌉
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ -
      ‖∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ / ‖cexp (I * Q x)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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 h1 : ‖cexp (I * Q x)‖ = 1 := by
  lift Q x to ℝ using hΘ Q hQ x with qx
  simp only [mul_comm I qx, norm_exp_ofReal_mul_I]
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
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ -
      ‖∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ / ‖cexp (I * Q x)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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

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)‖ -
      ‖∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ / ‖cexp (I * Q x)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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:
rw [h1, div_one]
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
⊢ ‖∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)‖ -
      ‖∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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

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)‖ -
      ‖∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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:
apply (norm_sub_norm_le _ _).trans
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
⊢ ‖(∫ (y : X) in {y | dist x y ∈ Ioo r R}, K x y * f y * cexp (I * Q y)) -
        ∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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

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)) -
        ∑ i ∈ Finset.Icc σ σ', ∫ (a : X), Ks K D ψ i x a * f a * cexp (I * Q a)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

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:
rw [← integral_finset_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
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

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:
simp_rw [← Finset.sum_mul]
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
⊢ ‖(∫ (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

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
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

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
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
Tactic:
rw [h3, ← neg_sub, ← integral_univ, ← integral_diff]
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)
⊢ ‖-∫ (x_1 : X) in univ \ {y | dist x y ∈ Ioo r R},
          (∑ i ∈ Finset.Icc σ σ', Ks K D ψ i x x_1) * f x_1 * cexp (I * Q x_1)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

case ht
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)
⊢ MeasurableSet {y | dist x y ∈ Ioo r R}

case hfs
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)
⊢ IntegrableOn (fun x_1 => (∑ i ∈ Finset.Icc σ σ', Ks K D ψ i x x_1) * f x_1 * cexp (I * Q x_1)) univ volume

case hts
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 | dist x y ∈ Ioo r R} ⊆ univ

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

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
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)
⊢ ‖-∫ (x_1 : X) in univ \ {y | dist x y ∈ Ioo r R},
          (∑ i ∈ Finset.Icc σ σ', Ks K D ψ i x x_1) * f x_1 * cexp (I * Q x_1)‖ ≤
    Ce3_1 a τ q * maximalFunction f x

case ht
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)
⊢ MeasurableSet {y | dist x y ∈ Ioo r R}

case hfs
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)
⊢ IntegrableOn (fun x_1 => (∑ i ∈ Finset.Icc σ σ', Ks K D ψ i x x_1) * f x_1 * cexp (I * Q x_1)) univ volume

case hts
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 | dist x y ∈ Ioo r R} ⊆ univ

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:
all_goals sorry
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
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))‖
⊢ 0 ≤ rhs
Tactic:
sorry
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
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)⌉
⊢ ‖cexp (I * Q x)‖ = 1
Tactic:
lift Q x to ℝ using hΘ Q hQ x with qx
State after:
case intro
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)⌉
qx : ℝ
⊢ ‖cexp (I * ↑qx)‖ = 1

State before:
case intro
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)⌉
qx : ℝ
⊢ ‖cexp (I * ↑qx)‖ = 1
Tactic:
simp only [mul_comm I qx, norm_exp_ofReal_mul_I]
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
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) =
    ∫ (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)
Tactic:
sorry
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
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:
sorry
State after:
no goals