internlm/Lean-Github huggingface dataset:
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
⊢ ‖∫ (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
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
⊢ ‖∫ (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 : ℝ
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)⌉
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)⌉
⊢ ‖∫ (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 : ℝ
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))‖
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)⌉
⊢ ‖∫ (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
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))‖
⊢ 0 ≤ rhs
Tactic:
sorry
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
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
Proof 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
Theorem: equation3_1
Proof 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]
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
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
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
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
Proof state after:
no goals
Theorem: equation2_2
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
hA : 1 < a
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hqq' : q.IsConjExponent q'
hF : MeasurableSet F
hG : MeasurableSet G
h2F : volume F ∈ Ioo 0 ⊤
h2G : volume G ∈ Ioo 0 ⊤
hT : NormBoundedBy (ANCZOperatorLp 2 K) (2 ^ a ^ 3)
⊢ ∃ G',
    volume G' ≤ volume G / 2 ∧
      ↑‖∫ (x : X) in G \ G', CarlesonOperator K Θ (F.indicator 1) x‖₊ ≤
        Ce2_2 a τ q * volume.real G ^ (1 / q') * volume.real F ^ (1 / q)
Tactic:
sorry
Proof state after:
no goals
Theorem: theorem1_2C
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
ha : 4 ≤ a
hq : q ∈ Ioc 1 2
hqq' : q.IsConjExponent q'
hF : MeasurableSet F
hG : MeasurableSet G
hT : NormBoundedBy (ANCZOperatorLp 2 K) 1
f : X → ℂ
hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x
⊢ ‖∫ (x : X) in G, CarlesonOperator K Θ f x‖ ≤ C1_2 a q * volume.real G ^ q'⁻¹ * volume.real F ^ q⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: theorem1_2C'
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
ha : 4 ≤ a
hq : q ∈ Ioc 1 2
hqq' : q.IsConjExponent q'
hF : MeasurableSet F
hG : MeasurableSet G
hT : NormBoundedBy (ANCZOperatorLp 2 K) 1
f : X → ℂ
hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : X) in G, CarlesonOperator' K Θ f x ≤ ENNReal.ofReal (C1_2 a q) * volume G ^ q'⁻¹ * volume F ^ q⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: dirichletKernel_periodic
Proof state before:
N : ℕ
⊢ Function.Periodic (dirichletKernel N) (2 * Real.pi)
Tactic:
sorry
Proof state after:
no goals
Theorem: dirichletKernel'_periodic
Proof state before:
N : ℕ
⊢ Function.Periodic (dirichletKernel' N) (2 * Real.pi)
Tactic:
sorry
Proof state after:
no goals
Theorem: dirichletKernel'_measurable
Proof state before:
N : ℕ
⊢ Measurable (dirichletKernel' N)
Tactic:
apply Measurable.add
Proof state after:
case hf
N : ℕ
⊢ Measurable fun a => cexp (I * ↑N * ↑a) / (1 - cexp (-I * ↑a))

case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Theorem: dirichletKernel'_measurable
Proof state before:
case hf
N : ℕ
⊢ Measurable fun a => cexp (I * ↑N * ↑a) / (1 - cexp (-I * ↑a))

case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Tactic:
. apply Measurable.div <;> measurability
Proof state after:
case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Theorem: dirichletKernel'_measurable
Proof state before:
case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Tactic:
. apply Measurable.div <;> measurability
Proof state after:
no goals
Theorem: dirichletKernel'_measurable
Proof state before:
case hf
N : ℕ
⊢ Measurable fun a => cexp (I * ↑N * ↑a) / (1 - cexp (-I * ↑a))
Tactic:
apply Measurable.div <;> measurability
Proof state after:
no goals
Theorem: dirichletKernel'_measurable
Proof state before:
case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Tactic:
apply Measurable.div <;> measurability
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ dirichletKernel N x = dirichletKernel' N x
Tactic:
have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
    = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
  calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
    _ = ∑ n in Icc (-Int.ofNat N) ↑N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
      rw [dirichletKernel, mul_sum]
      congr
      ext n
      simp [sub_mul, ← exp_add, ← exp_add]
      congr <;>
      . ring_nf
        congr 1
        rw [mul_assoc, mul_assoc]
        congr
        rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
        norm_cast
        exact Real.pi_pos.ne.symm
    _ = ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n - 1 / 2) * I * ↑x) := by
      rw [sum_sub_distrib]
    _ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
      rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm]
      symm
      rw [← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
      congr
      symm
      rw [sub_eq_zero]
      conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
      congr
      . ext n
        rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc]
      . ext n
        congr
        simp [add_assoc, sub_eq_add_neg]
        congr
        norm_num
      . rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
        norm_cast
      all_goals simp
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
⊢ dirichletKernel N x = dirichletKernel' N x
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
⊢ dirichletKernel N x = dirichletKernel' N x
Tactic:
have h' : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) ≠ 0 := by
  contrapose! h
  rw [sub_eq_zero] at h
  calc cexp (I * ↑x)
    _ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by
      rw [← exp_add]
      congr
      rw [mul_assoc, ← mul_add]
      ring
    _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by
      congr
    _ = 1 := by
      rw [← exp_add]
      ring_nf
      exact exp_zero
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = dirichletKernel' N x
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = dirichletKernel' N x
Tactic:
rw [dirichletKernel']
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))
Tactic:
apply mul_left_cancel₀ h'
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) *
      (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) *
      (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
rw [this, mul_add, sub_eq_add_neg]
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) + -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))) +
      (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) + -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))) +
      (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
congr
Proof state after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)))

case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Theorem: dirichletKernel_eq
Proof state before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)))

case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
. rw [mul_div]
  apply eq_div_of_mul_eq
  . contrapose! h
    rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
  ring_nf
  rw [← exp_add, ← exp_add, ← exp_add]
  congr 2 <;> ring
Proof state after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))