noncomputable def Θ' (X : Type u_1) {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] : Set (Θ X)

A countable dense subset of Θ X.

Equations

• Θ' X = ⋯.choose

theorem countable_Θ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] : (Θ' X).Countable

theorem dense_Θ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] : Dense (Θ' X)

def J102 : Set (ℚ × ℚ)

A countable dense subset of the range of R₁ and R₂.

Equations

• J102 = {p : ℚ × ℚ | 0 < p.1 ∧ p.1 < p.2}

theorem carlesonOperator_eq_biSup_Θ'_J102 {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {x : X} (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ 1) : carlesonOperator K f x = ⨆ θ ∈ Θ' X, ⨆ j ∈ J102, ‖carlesonOperatorIntegrand K θ (↑j.1) (↑j.2) f x‖ₑ

noncomputable def enumΘ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) : ℕ → ↑(Θ' X)

An enumeration of Θ' X, assuming it is nonempty. It may contain duplicates.

Equations

• enumΘ' nΘ' = ⋯.choose

theorem surjective_enumΘ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) : Function.Surjective (enumΘ' nΘ')

theorem biSup_Θ'_eq_biSup_enumΘ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) (g : Θ X → X → ENNReal) {x : X} : ⨆ θ ∈ Θ' X, g θ x = ⨆ (n : ℕ), ⨆ i ∈ Finset.range (n + 1), g (↑(enumΘ' nΘ' i)) x

noncomputable def enumΘ'ArgMax {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) (g : Θ X → X → ENNReal) (n : ℕ) (x : X) : ℕ

The argmax of g (enumΘ' nΘ' i) x over i ≤ n with lower indices winning ties.

Equations

• enumΘ'ArgMax nΘ' g n x = List.findIdx (fun (i : ℕ) => decide (∀ j ≤ n, g (↑(enumΘ' nΘ' j)) x ≤ g (↑(enumΘ' nΘ' i)) x)) (List.range (n + 1))

theorem enumΘ'ArgMax_mem_range {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) (g : Θ X → X → ENNReal) {n : ℕ} {x : X} : enumΘ'ArgMax nΘ' g n x ∈ Finset.range (n + 1)

theorem enumΘ'ArgMax_eq_iff {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) (g : Θ X → X → ENNReal) {n i : ℕ} {x : X} (hi : i ≤ n) : enumΘ'ArgMax nΘ' g n x = i ↔ (∀ j ≤ n, g (↑(enumΘ' nΘ' j)) x ≤ g (↑(enumΘ' nΘ' i)) x) ∧ ∀ j < i, g (↑(enumΘ' nΘ' j)) x < g (↑(enumΘ' nΘ' i)) x

The characterising property of enumΘ'ArgMax.

noncomputable def QΘ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) {g : Θ X → X → ENNReal} (mg : ∀ (θ : Θ X), Measurable (g θ)) (n : ℕ) : MeasureTheory.SimpleFunc X (Θ X)

The simple function corresponding to the blueprint's Q_n.

Equations

• QΘ' nΘ' mg n = { toFun := fun (x : X) => ↑(enumΘ' nΘ' (enumΘ'ArgMax nΘ' g n x)), measurableSet_fiber' := ⋯, finite_range' := ⋯ }

theorem biSup_enumΘ'_le_QΘ' {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (nΘ' : (Θ' X).Nonempty) {g : Θ X → X → ENNReal} (mg : ∀ (θ : Θ X), Measurable (g θ)) {n : ℕ} {x : X} : ⨆ i ∈ Finset.range (n + 1), g (↑(enumΘ' nΘ' i)) x ≤ g ((QΘ' nΘ' mg n) x) x

theorem lowerSemicontinuous_LNT {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {Q : MeasureTheory.SimpleFunc X (Θ X)} {θ : Θ X} : LowerSemicontinuous (linearizedNontangentialOperator (⇑Q) θ K f)

theorem BST_LNT_of_BST_NT {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} (hT : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => nontangentialOperator K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) (θ : Θ X) : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)

theorem metric_carleson {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) (hT : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => nontangentialOperator K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, carlesonOperator K f x ≤ ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

Theorem 1.1.1

theorem metric_carleson_check : MetricSpaceCarleson

theorem metric_carleson' {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) (hT : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => nontangentialOperator K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, carlesonOperator K f x ≤ 2 ^ (443 * a ^ 3) / (↑q - 1) ^ 6 * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹