theorem continuous_carlesonOperatorIntegrand.{u_1}continuous_carlesonOperatorIntegrand.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K]
  {R₁ R₂ : ℝ} {f : X → ℂ} {x : X} (mf : Measurable f) (nf : (fun x ↦ ‖f x‖) ≤ 1) (hR₁ : 0 < R₁) :
  Continuous fun x_1 ↦ carlesonOperatorIntegrand K x_1 R₁ R₂ f x
  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1]
  {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {R₁ℝ R₂ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } {xX : XType u_1}
  (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ)
  (nf(fun x ↦ ‖f x‖) ≤ 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (hR₁0 < R₁ : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. R₁ℝ) :
  ContinuousContinuous.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : PropA function between topological spaces is continuous if the preimage
of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.  fun x_1Θ X ↦
    carlesonOperatorIntegrandcarlesonOperatorIntegrand.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂThe integrand in the (linearized) Carleson operator.
This is `G` in Lemma 3.0.1.  KX → X → ℂ x_1Θ X R₁ℝ R₂ℝ
      fX → ℂ xX

theorem rightContinuous_carlesonOperatorIntegrand.{u_1}rightContinuous_carlesonOperatorIntegrand.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ}
  [KernelProofData a K] {θ : Θ X} {R₁ R₂ : ℝ} {f : X → ℂ} {x : X} (mf : Measurable f) (nf : (fun x ↦ ‖f x‖) ≤ 1)
  (hR₁ : 0 < R₁) : ContinuousWithinAt (fun x_1 ↦ carlesonOperatorIntegrand K θ x_1 R₂ f x) (Set.Ici R₁) R₁
  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1]
  {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {θΘ X : ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1} {R₁ℝ R₂ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  {xX : XType u_1} (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ)
  (nf(fun x ↦ ‖f x‖) ≤ 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (hR₁0 < R₁ : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. R₁ℝ) :
  ContinuousWithinAtContinuousWithinAt.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y)
  (s : Set X) (x : X) : PropA function between topological spaces is continuous at a point `x₀` within a subset `s`
if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. 
    (fun x_1ℝ ↦
      carlesonOperatorIntegrandcarlesonOperatorIntegrand.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂThe integrand in the (linearized) Carleson operator.
This is `G` in Lemma 3.0.1.  KX → X → ℂ θΘ X x_1ℝ R₂ℝ
        fX → ℂ xX)
    (Set.IciSet.Ici.{u_1} {α : Type u_1} [Preorder α] (b : α) : Set α`Ici a` is the left-closed right-infinite interval $[a, ∞)$.  R₁ℝ) R₁ℝ

theorem leftContinuous_carlesonOperatorIntegrand.{u_1}leftContinuous_carlesonOperatorIntegrand.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ}
  [KernelProofData a K] {θ : Θ X} {R₁ R₂ : ℝ} {f : X → ℂ} {x : X} (mf : Measurable f) (nf : (fun x ↦ ‖f x‖) ≤ 1)
  (hR₁ : 0 < R₁) : ContinuousWithinAt (fun x_1 ↦ carlesonOperatorIntegrand K θ R₁ x_1 f x) (Set.Iic R₂) R₂
  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1]
  {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {θΘ X : ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1} {R₁ℝ R₂ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  {xX : XType u_1} (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ)
  (nf(fun x ↦ ‖f x‖) ≤ 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (hR₁0 < R₁ : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. R₁ℝ) :
  ContinuousWithinAtContinuousWithinAt.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y)
  (s : Set X) (x : X) : PropA function between topological spaces is continuous at a point `x₀` within a subset `s`
if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. 
    (fun x_1ℝ ↦
      carlesonOperatorIntegrandcarlesonOperatorIntegrand.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂThe integrand in the (linearized) Carleson operator.
This is `G` in Lemma 3.0.1.  KX → X → ℂ θΘ X R₁ℝ x_1ℝ
        fX → ℂ xX)
    (Set.IicSet.Iic.{u_1} {α : Type u_1} [Preorder α] (b : α) : Set α`Iic b` is the left-infinite right-closed interval $(-∞, b]$.  R₂ℝ) R₂ℝ

theorem measurable_carlesonOperatorIntegrand.{u_1}measurable_carlesonOperatorIntegrand.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K]
  {Q : MeasureTheory.SimpleFunc X (Θ X)} {R₁ R₂ : ℝ} {f : X → ℂ} (mf : Measurable f) :
  Measurable fun x ↦ carlesonOperatorIntegrand K (Q x) R₁ R₂ f x
  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1]
  {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {QMeasureTheory.SimpleFunc X (Θ X) : MeasureTheory.SimpleFuncMeasureTheory.SimpleFunc.{u, v} (α : Type u) [MeasurableSpace α] (β : Type v) : Type (max u v)A function `f` from a measurable space to any type is called *simple*,
if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles
a function with these properties.  XType u_1 (ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1)}
  {R₁ℝ R₂ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ) :
  MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fun xX ↦
    carlesonOperatorIntegrandcarlesonOperatorIntegrand.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂThe integrand in the (linearized) Carleson operator.
This is `G` in Lemma 3.0.1.  KX → X → ℂ (QMeasureTheory.SimpleFunc X (Θ X) xX) R₁ℝ
      R₂ℝ fX → ℂ xX

theorem enorm_carlesonOperatorIntegrand_le.{u_1}enorm_carlesonOperatorIntegrand_le.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K]
  {θ : Θ X} {f : X → ℂ} {x : X} {R₁ R₂ : NNReal} (nf : (fun x ↦ ‖f x‖) ≤ 1) (hR₁ : 0 < R₁) :
  ‖carlesonOperatorIntegrand K θ (↑R₁) (↑R₂) f x‖ₑ ≤ ↑(C3_0_1 a R₁ R₂)
  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1]
  {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {θΘ X : ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1} {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } {xX : XType u_1}
  {R₁NNReal R₂NNReal : NNRealNNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace }
  (nf(fun x ↦ ‖f x‖) ≤ 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (hR₁0 < R₁ : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. R₁NNReal) :
  ‖ENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function. carlesonOperatorIntegrandcarlesonOperatorIntegrand.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂThe integrand in the (linearized) Carleson operator.
This is `G` in Lemma 3.0.1.  KX → X → ℂ θΘ X (↑R₁NNReal)
        (↑R₂NNReal) fX → ℂ xX‖ₑENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    ↑(C3_0_1C3_0_1 (a : ℕ) (R₁ R₂ : NNReal) : NNRealThe constant used in the proof of `int-continuous`.  aℕ R₁NNReal R₂NNReal)

theorem R_truncation.{u_1}R_truncation.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ}
  [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {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 ↦ ‖f x‖) ≤ F.indicator 1) {n : ℕ} {R : ℝ} (hR : R = 2 ^ n)
  (BST_T_Q :
    ∀ (θ : Θ X),
      MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
        MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) :
  ∫⁻ (x : X) in G, ⨆ R₁ ∈ Set.Ioo R⁻¹ R, ⨆ R₂ ∈ Set.Ioo R₁ R, ‖T_R K Q R₁ R₂ R f x‖ₑ ≤
    ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹Lemma 3.0.2.  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1] {qNNReal q'NNReal : NNRealNNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace }
  {FSet X GSet X : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 XType u_1} {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {QMeasureTheory.SimpleFunc X (Θ X) : MeasureTheory.SimpleFuncMeasureTheory.SimpleFunc.{u, v} (α : Type u) [MeasurableSpace α] (β : Type v) : Type (max u v)A function `f` from a measurable space to any type is called *simple*,
if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles
a function with these properties.  XType u_1 (ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1)}
  {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  [IsCancellativeIsCancellative.{u_2} (X : Type u_2) {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] (τ : ℝ)
  [CompatibleFunctions ℝ X A] : PropΘ is τ-cancellative. `τ` will usually be `1 / a`  XType u_1 (defaultτdefaultτ (a : ℕ) : ℝ`defaultτ` is the inverse of `a`.  aℕ)]
  (hqq ∈ Set.Ioc 1 2 : qNNReal ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IocSet.Ioc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioc a b` is the left-open right-closed interval $(a, b]$.  1 2)
  (hqq'q.HolderConjugate q' : qNNReal.HolderConjugateNNReal.HolderConjugate (p q : NNReal) : PropNonnegative real numbers `p q : ℝ≥0` are **Hölder conjugate** if they are positive and satisfy
the equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `NNReal.HolderTriple p q 1`. This
condition shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `NNReal.holderConjugate_iff`.  q'NNReal)
  (mFMeasurableSet F : MeasurableSetMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  FSet X)
  (mGMeasurableSet G : MeasurableSetMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  GSet X)
  (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ)
  (nf(fun x ↦ ‖f x‖) ≤ F.indicator 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. FSet X.indicatorSet.indicator.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (x : α) : M`Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  1)
  {nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} {Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hRR = 2 ^ n : Rℝ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. nℕ)
  (BST_T_Q∀ (θ : Θ X),
  MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
    MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a) :
    ∀ (θΘ X : ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1),
      MeasureTheory.HasBoundedStrongTypeMeasureTheory.HasBoundedStrongType.{u_4, u_5, u_12, u_13} {ε₁ : Type u_4} {ε₂ : Type u_5} [ENorm ε₁] [ENorm ε₂]
  [TopologicalSpace ε₁] [TopologicalSpace ε₂] {α : Type u_12} {α' : Type u_13} [Zero ε₁] {_x : MeasurableSpace α}
  {_x' : MeasurableSpace α'} (T : (α → ε₁) → α' → ε₂) (p p' : ENNReal) (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure α') (c : ENNReal) : PropA weaker version of `HasStrongType`. This is the same as `HasStrongType` if `T` is continuous
w.r.t. the L^2 norm, but weaker in general. 
        (fun x1X → ℂ x2X ↦
          linearizedNontangentialOperatorlinearizedNontangentialOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X]
  [hXA : MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (K : X → X → ℂ) (f : X → ℂ)
  (x : X) : ENNRealThe linearized maximally truncated nontangential Calderon–Zygmund operator `T_Q^θ`. 
            (⇑QMeasureTheory.SimpleFunc X (Θ X)) θΘ X KX → X → ℂ x1X → ℂ x2X)
        2 2 MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  ↑(C_TsC_Ts (a : ℕ) : NNRealA constant used on the boundedness of `T_Q^θ` and `T_*`. We generally assume
`HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·) 2 2 volume volume (C_Ts a)`
throughout this formalization.  aℕ)) :
  ∫⁻MeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  (xX : XType u_1) inMeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  GSet X,MeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`. 
      ⨆ R₁ℝ ∈ Set.IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioo a b` is the left-open right-open interval $(a, b)$.  Rℝ⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. Rℝ,
        ⨆ R₂ℝ ∈ Set.IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioo a b` is the left-open right-open interval $(a, b)$.  R₁ℝ Rℝ,
          ‖ENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function. T_RT_R.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] :
  (X → X → ℂ) → (Q : MeasureTheory.SimpleFunc X (Θ X)) → (R₁ R₂ R : ℝ) → (f : X → ℂ) → (x : X) → ℂThe operator T_{R₁, R₂, R} introduced in Lemma 3.0.2.  KX → X → ℂ QMeasureTheory.SimpleFunc X (Θ X) R₁ℝ R₂ℝ Rℝ fX → ℂ xX‖ₑENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    ↑(C1_0_2C1_0_2 (a : ℕ) (q : NNReal) : NNRealThe constant used in `MetricSpaceCarleson` and `LinearizedMetricCarleson`.
Has value `2 ^ (443 * a ^ 3) / (q - 1) ^ 6` in the blueprint.  aℕ qNNReal) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  GSet X ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (↑q'NNReal)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  FSet X ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (↑qNNReal)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.

theorem S_truncation.{u_1}S_truncation.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ}
  [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} [IsCancellative X (defaultτ a)] {B : ℕ}
  (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (bF : Bornology.IsBounded F) (bG : Bornology.IsBounded G)
  (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun x ↦ ‖f x‖) ≤ F.indicator 1)
  (BST_T_Q :
    ∀ (θ : Θ X),
      MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
        MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) :
  ∫⁻ (x : X) in G, ⨆ s₁ ∈ Finset.Icc (-↑B) ↑B, ⨆ s₂ ∈ Finset.Icc s₁ ↑B, ‖T_S Q s₁ s₂ f x‖ₑ ≤
    ↑(C3_0_4 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹Lemma 3.0.3. `B` is the blueprint's `S`.  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1] {qNNReal q'NNReal : NNRealNNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace }
  {FSet X GSet X : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 XType u_1} {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {QMeasureTheory.SimpleFunc X (Θ X) : MeasureTheory.SimpleFuncMeasureTheory.SimpleFunc.{u, v} (α : Type u) [MeasurableSpace α] (β : Type v) : Type (max u v)A function `f` from a measurable space to any type is called *simple*,
if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles
a function with these properties.  XType u_1 (ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1)}
  {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  [IsCancellativeIsCancellative.{u_2} (X : Type u_2) {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] (τ : ℝ)
  [CompatibleFunctions ℝ X A] : PropΘ is τ-cancellative. `τ` will usually be `1 / a`  XType u_1 (defaultτdefaultτ (a : ℕ) : ℝ`defaultτ` is the inverse of `a`.  aℕ)] {Bℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (hqq ∈ Set.Ioc 1 2 : qNNReal ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IocSet.Ioc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioc a b` is the left-open right-closed interval $(a, b]$.  1 2)
  (hqq'q.HolderConjugate q' : qNNReal.HolderConjugateNNReal.HolderConjugate (p q : NNReal) : PropNonnegative real numbers `p q : ℝ≥0` are **Hölder conjugate** if they are positive and satisfy
the equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `NNReal.HolderTriple p q 1`. This
condition shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `NNReal.holderConjugate_iff`.  q'NNReal)
  (bFBornology.IsBounded F : Bornology.IsBoundedBornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : Prop`IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  FSet X)
  (bGBornology.IsBounded G : Bornology.IsBoundedBornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : Prop`IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  GSet X)
  (mFMeasurableSet F : MeasurableSetMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  FSet X)
  (mGMeasurableSet G : MeasurableSetMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  GSet X)
  (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ)
  (nf(fun x ↦ ‖f x‖) ≤ F.indicator 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. FSet X.indicatorSet.indicator.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (x : α) : M`Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  1)
  (BST_T_Q∀ (θ : Θ X),
  MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
    MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a) :
    ∀ (θΘ X : ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1),
      MeasureTheory.HasBoundedStrongTypeMeasureTheory.HasBoundedStrongType.{u_4, u_5, u_12, u_13} {ε₁ : Type u_4} {ε₂ : Type u_5} [ENorm ε₁] [ENorm ε₂]
  [TopologicalSpace ε₁] [TopologicalSpace ε₂] {α : Type u_12} {α' : Type u_13} [Zero ε₁] {_x : MeasurableSpace α}
  {_x' : MeasurableSpace α'} (T : (α → ε₁) → α' → ε₂) (p p' : ENNReal) (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure α') (c : ENNReal) : PropA weaker version of `HasStrongType`. This is the same as `HasStrongType` if `T` is continuous
w.r.t. the L^2 norm, but weaker in general. 
        (fun x1X → ℂ x2X ↦
          linearizedNontangentialOperatorlinearizedNontangentialOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X]
  [hXA : MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (K : X → X → ℂ) (f : X → ℂ)
  (x : X) : ENNRealThe linearized maximally truncated nontangential Calderon–Zygmund operator `T_Q^θ`. 
            (⇑QMeasureTheory.SimpleFunc X (Θ X)) θΘ X KX → X → ℂ x1X → ℂ x2X)
        2 2 MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  ↑(C_TsC_Ts (a : ℕ) : NNRealA constant used on the boundedness of `T_Q^θ` and `T_*`. We generally assume
`HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·) 2 2 volume volume (C_Ts a)`
throughout this formalization.  aℕ)) :
  ∫⁻MeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  (xX : XType u_1) inMeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  GSet X,MeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`. 
      ⨆ s₁ℤ ∈ Finset.IccFinset.Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset αThe finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
finset.  (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).↑Bℕ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator). ↑Bℕ,
        ⨆ s₂ℤ ∈ Finset.IccFinset.Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset αThe finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
finset.  s₁ℤ ↑Bℕ,
          ‖ENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function. T_ST_S.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K]
  (Q : MeasureTheory.SimpleFunc X (Θ X)) (s₁ s₂ : ℤ) (f : X → ℂ) (x : X) : ℂThe operator T_{s₁, s₂} introduced in Lemma 3.0.3.  QMeasureTheory.SimpleFunc X (Θ X) s₁ℤ s₂ℤ fX → ℂ xX‖ₑENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    ↑(C3_0_4C3_0_4 (a : ℕ) (q : NNReal) : NNRealThe constant used in `linearized_truncation` and `S_truncation`.
Has value `2 ^ (442 * a ^ 3 + 2)` in the blueprint.  aℕ qNNReal) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  GSet X ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (↑q'NNReal)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  FSet X ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (↑qNNReal)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.

theorem linearized_truncation.{u_1}linearized_truncation.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ}
  [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {σ₁ σ₂ : X → ℤ}
  [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (bF : Bornology.IsBounded F)
  (bG : Bornology.IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f)
  (nf : (fun x ↦ ‖f x‖) ≤ F.indicator 1) (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂) (rσ₁ : (Set.range σ₁).Finite)
  (rσ₂ : (Set.range σ₂).Finite) (lσ : σ₁ ≤ σ₂)
  (BST_T_Q :
    ∀ (θ : Θ X),
      MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
        MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) :
  ∫⁻ (x : X) in G, ‖T_lin Q σ₁ σ₂ f x‖ₑ ≤
    ↑(C3_0_4 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹Lemma 3.0.4.  {XType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {aℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [MetricSpaceMetricSpace.{u} (α : Type u) : Type uA metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  XType u_1] {qNNReal q'NNReal : NNRealNNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace }
  {FSet X GSet X : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 XType u_1} {KX → X → ℂ : XType u_1 → XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  [KernelProofDataKernelProofData.{u_1} {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)Data common through most of chapters 2-7.
These contain the minimal axioms for `kernel-summand`'s proof.
This is used in chapter 3 when we don't have all other fields from `ProofData`.  aℕ KX → X → ℂ]
  {QMeasureTheory.SimpleFunc X (Θ X) : MeasureTheory.SimpleFuncMeasureTheory.SimpleFunc.{u, v} (α : Type u) [MeasurableSpace α] (β : Type v) : Type (max u v)A function `f` from a measurable space to any type is called *simple*,
if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles
a function with these properties.  XType u_1 (ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1)}
  {fX → ℂ : XType u_1 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } {σ₁X → ℤ σ₂X → ℤ : XType u_1 → ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
}
  [IsCancellativeIsCancellative.{u_2} (X : Type u_2) {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] (τ : ℝ)
  [CompatibleFunctions ℝ X A] : PropΘ is τ-cancellative. `τ` will usually be `1 / a`  XType u_1 (defaultτdefaultτ (a : ℕ) : ℝ`defaultτ` is the inverse of `a`.  aℕ)]
  (hqq ∈ Set.Ioc 1 2 : qNNReal ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IocSet.Ioc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioc a b` is the left-open right-closed interval $(a, b]$.  1 2)
  (hqq'q.HolderConjugate q' : qNNReal.HolderConjugateNNReal.HolderConjugate (p q : NNReal) : PropNonnegative real numbers `p q : ℝ≥0` are **Hölder conjugate** if they are positive and satisfy
the equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `NNReal.HolderTriple p q 1`. This
condition shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `NNReal.holderConjugate_iff`.  q'NNReal)
  (bFBornology.IsBounded F : Bornology.IsBoundedBornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : Prop`IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  FSet X)
  (bGBornology.IsBounded G : Bornology.IsBoundedBornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : Prop`IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  GSet X)
  (mFMeasurableSet F : MeasurableSetMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  FSet X)
  (mGMeasurableSet G : MeasurableSetMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)  GSet X)
  (mfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fX → ℂ)
  (nf(fun x ↦ ‖f x‖) ≤ F.indicator 1 : (fun xX ↦ ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fX → ℂ xX‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. FSet X.indicatorSet.indicator.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (x : α) : M`Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  1)
  (mσ₁Measurable σ₁ : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  σ₁X → ℤ)
  (mσ₂Measurable σ₂ : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  σ₂X → ℤ)
  (rσ₁(Set.range σ₁).Finite : (Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  σ₁X → ℤ).FiniteSet.Finite.{u} {α : Type u} (s : Set α) : PropA set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`. )
  (rσ₂(Set.range σ₂).Finite : (Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  σ₂X → ℤ).FiniteSet.Finite.{u} {α : Type u} (s : Set α) : PropA set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`. )
  (lσσ₁ ≤ σ₂ : σ₁X → ℤ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. σ₂X → ℤ)
  (BST_T_Q∀ (θ : Θ X),
  MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
    MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a) :
    ∀ (θΘ X : ΘFunctionDistances.Θ.{u, u_3} {𝕜 : outParam (Type u_3)} (X : Type u) {inst✝ : NormedField 𝕜}
  {inst✝¹ : TopologicalSpace X} [self : FunctionDistances 𝕜 X] : Type uA type of continuous functions from `X` to `𝕜`.  XType u_1),
      MeasureTheory.HasBoundedStrongTypeMeasureTheory.HasBoundedStrongType.{u_4, u_5, u_12, u_13} {ε₁ : Type u_4} {ε₂ : Type u_5} [ENorm ε₁] [ENorm ε₂]
  [TopologicalSpace ε₁] [TopologicalSpace ε₂] {α : Type u_12} {α' : Type u_13} [Zero ε₁] {_x : MeasurableSpace α}
  {_x' : MeasurableSpace α'} (T : (α → ε₁) → α' → ε₂) (p p' : ENNReal) (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure α') (c : ENNReal) : PropA weaker version of `HasStrongType`. This is the same as `HasStrongType` if `T` is continuous
w.r.t. the L^2 norm, but weaker in general. 
        (fun x1X → ℂ x2X ↦
          linearizedNontangentialOperatorlinearizedNontangentialOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X]
  [hXA : MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (K : X → X → ℂ) (f : X → ℂ)
  (x : X) : ENNRealThe linearized maximally truncated nontangential Calderon–Zygmund operator `T_Q^θ`. 
            (⇑QMeasureTheory.SimpleFunc X (Θ X)) θΘ X KX → X → ℂ x1X → ℂ x2X)
        2 2 MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  ↑(C_TsC_Ts (a : ℕ) : NNRealA constant used on the boundedness of `T_Q^θ` and `T_*`. We generally assume
`HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·) 2 2 volume volume (C_Ts a)`
throughout this formalization.  aℕ)) :
  ∫⁻MeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  (xX : XType u_1) inMeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  GSet X,MeasureTheory.lintegral.{u_4} {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
  ENNRealThe **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  ‖ENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function. T_linT_lin.{u_1} {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K]
  (Q : MeasureTheory.SimpleFunc X (Θ X)) (σ₁ σ₂ : X → ℤ) (f : X → ℂ) (x : X) : ℂThe operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4.  QMeasureTheory.SimpleFunc X (Θ X) σ₁X → ℤ σ₂X → ℤ fX → ℂ xX‖ₑENorm.enorm.{u_8} {E : Type u_8} [self : ENorm E] : E → ENNRealthe `ℝ≥0∞`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    ↑(C3_0_4C3_0_4 (a : ℕ) (q : NNReal) : NNRealThe constant used in `linearized_truncation` and `S_truncation`.
Has value `2 ^ (442 * a ^ 3 + 2)` in the blueprint.  aℕ qNNReal) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  GSet X ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (↑q'NNReal)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  FSet X ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (↑qNNReal)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.