Carleson Blueprint

1.1. Introduction🔗

Trigonometric series represent functions as possibly infinite linear combinations of pure frequencies. They gained particular prominence through the work of J. Fourier, who used them in his analytical theory of heat, thereby establishing them as a tool for solving partial differential equations. Fourier also made the groundbreaking claim that a wide range of functions could be represented using trigonometric series. This sparked the interest of many mathematicians, including Dirichlet, who gave some rigorous conditions for convergence of Fourier series, as trigonometric series are now called. Dirichlet also opened a branch of analytic number theory partially inspired by the ideas of Fourier. Nowadays, Fourier analysis plays an important role in many areas of mathematics.

With Euler's formula to represent pure frequencies in mind, a trigonometric polynomial can be expressed as S_N(x):= \sum_{n=-N}^N c_n e^{inx}. The Fourier series is then defined as the limit f of such a sequence S_N as N tends to \infty. Fourier's vision to represent rather general functions raises two fundamental questions. The first question is to identify the appropriate choice of coefficients c_n to use to represent a given f. The second question addresses the convergence of S_N to f.

The first question has a fairly canonical and standard answer, provided by the Fourier integral formula: c_n := \widehat{f}_n := \frac 1{2\pi}\int_0^{2\pi} f(x)e^{-inx}\, dx. Here the precise interpretation of the integral depends on the chosen theory of integration. For a continuous function f, Riemann's notion of the integral suffices. If f is integrable in the Lebesgue sense, f \in L^1(0,2\pi), the Lebesgue integral is appropriate. More generally, if f is a distribution in the sense of Schwartz, supported in [0,2\pi], the integral can be understood as an evaluation against the periodic test function e^{-inx}. In each case, the more general definition reduces to the simpler one within the respective more restrictive domain. Hence, the Fourier coefficients given above serve as a universal choice. This choice is unique in several respects, in particular if one is to exactly reproduce a trigonometric polynomial f.

The second question of convergence bifurcates into the question of pointwise convergence of the series with coefficients given above for a given x on the one hand and convergence of the functions S_N to the function f in a suitable function space with corresponding topology on the other hand. There are at least as many function spaces for the question of convergence as there are different definitions of the integral elaborated earlier. There are some very canonical answers to the convergence question in function spaces, albeit not known at the time of Fourier and Dirichlet. One example is convergence in the Hilbert space sense for f in L^2(0,2\pi), as discovered in the first decade of the twentieth century as a consequence of the rapid development of Lebesgue integration theory. Another canonical example is convergence in the sense of distributions for general distributional f, as discovered a few decades after Lebesgue integration. For some other natural spaces, such as L^1(0,2\pi), there is no guarantee of convergence in the norm of that space even if f is in the space.

In contrast to these examples of function spaces with a very natural theory of convergence of Fourier series in the topology of the function space, there are no similarly elegant solutions to the characterization of pointwise convergence. In particular, the space of functions f such that the sequence S_N(x) converges for every x does not have a good characterization in terms of f itself. Similarly, the space of all functions f such that the sequence of coefficients \widehat{f}_n is absolutely summable has also no good characterization.

When the Fourier integral is defined in the Lebesgue sense and f \in L^1(0,2\pi), then the function f itself is meaningful not everywhere but only pointwise almost everywhere in the Lebesgue sense. The question of pointwise convergence to f for all x then becomes meaningless, and instead one asks for almost everywhere convergence. Such convergence was conjectured by N. Luzin for the space L^2(0,2\pi). Kolmogorov's example of an L^1 function whose Fourier series diverges at almost every point seemed to provide some evidence against Luzin's conjecture. Indeed, in the 1960s, L. Carleson tried to construct a counterexample to Luzin's conjecture. In his own recollection, his efforts led him to better and better understand how such a potential counterexample should look like. In the end, the counterexample had to satisfy so many properties that the properties started to contradict each other, and Carleson realized that a counterexample could not exist. Thus, he had proved Luzin's conjecture. In particular, he had proven the more elementary statement

Theorem1.1
✓L∃∀Nused by 0

Uses [??]. Let f be a 2\pi-periodic complex-valued continuous function on \mathbb{R}. Then for almost all x \in \mathbb{R} we have \lim_{N\to\infty} S_N f(x) = f(x), where S_N f is the N-th partial Fourier sum defined above with Fourier coefficients defined above.

Lean code for Theorem1.1●1 theorem
  • theoremdefined in Carleson/Classical/ClassicalCarleson.lean
    complete
    theorem classical_carlesonclassical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) :
  ∀ᵐ (x : ℝ), Filter.Tendsto (fun x_1 ↦ partialFourierSum x_1 f x) Filter.atTop (nhds (f x)) {fℝ → ℂ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } (cont_fContinuous f : 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.  fℝ → ℂ)
  (periodic_fFunction.Periodic f (2 * Real.pi) : Function.PeriodicFunction.Periodic.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Add α] (f : α → β) (c : α) : PropA function `f` is said to be `Periodic` with period `c` if for all `x`, `f (x + c) = f x`.  fℝ → ℂ (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`.2 *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`. Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened. )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`.) :
  ∀ᵐFilter.Eventually.{u_1} {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop`f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`.  (xℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ),Filter.Eventually.{u_1} {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop`f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`. 
    Filter.TendstoFilter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop`Filter.Tendsto` is the generic "limit of a function" predicate.
`Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
the `f`-preimage of `a` is an `l₁` neighborhood.  (fun x_1ℕ ↦ partialFourierSumpartialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂThe Nᵗʰ partial Fourier sum of `f : ℝ → ℂ` for `N : ℕ`.  x_1ℕ fℝ → ℂ xℝ) Filter.atTopFilter.atTop.{u_3} {α : Type u_3} [Preorder α] : Filter α`atTop` is the filter representing the limit `→ ∞` on an ordered set.
It is generated by the collection of up-sets `{b | a ≤ b}`.
(The preorder need not have a top element for this to be well defined,
and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.) 
      (nhdsnhds.{u_3} {X : Type u_3} [TopologicalSpace X] (x : X) : Filter XA set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`.  (fℝ → ℂ xℝ))
    theorem classical_carlesonclassical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) :
  ∀ᵐ (x : ℝ), Filter.Tendsto (fun x_1 ↦ partialFourierSum x_1 f x) Filter.atTop (nhds (f x)) {fℝ → ℂ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  (cont_fContinuous f : 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.  fℝ → ℂ)
  (periodic_fFunction.Periodic f (2 * Real.pi) :
    Function.PeriodicFunction.Periodic.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Add α] (f : α → β) (c : α) : PropA function `f` is said to be `Periodic` with period `c` if for all `x`, `f (x + c) = f x`.  fℝ → ℂ (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`.2 *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`. Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened. )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`.) :
  ∀ᵐFilter.Eventually.{u_1} {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop`f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`.  (xℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ),Filter.Eventually.{u_1} {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop`f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`. 
    Filter.TendstoFilter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop`Filter.Tendsto` is the generic "limit of a function" predicate.
`Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
the `f`-preimage of `a` is an `l₁` neighborhood. 
      (fun x_1ℕ ↦
        partialFourierSumpartialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂThe Nᵗʰ partial Fourier sum of `f : ℝ → ℂ` for `N : ℕ`.  x_1ℕ fℝ → ℂ xℝ)
      Filter.atTopFilter.atTop.{u_3} {α : Type u_3} [Preorder α] : Filter α`atTop` is the filter representing the limit `→ ∞` on an ordered set.
It is generated by the collection of up-sets `{b | a ≤ b}`.
(The preorder need not have a top element for this to be well defined,
and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.)  (nhdsnhds.{u_3} {X : Type u_3} [TopologicalSpace X] (x : X) : Filter XA set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`.  (fℝ → ℂ xℝ))

Here, almost every x means in the Lebesgue sense, that is, for every \epsilon > 0 the set of x where convergence fails can be covered by a sequence of intervals such that the sum of the lengths of these intervals is less than \epsilon. While Carleson had proven the more general Luzin conjecture for functions in L^2[0,2\pi], even the more elementary statement for continuous functions was not known before Carleson's work. Moreover, until now, the elementary statement has not seen any substantially easier proof than those generalizing to L^2, partially because there is no readily usable criterion on the level of Fourier coefficients to distinguish between continuous functions and L^2 functions.

Shortly after Carleson's breakthrough, Hunt proved the analogous result for L^p functions with p > 1 and for functions in L^1\log(L)^2. Billard adapted Carleson's arguments to prove almost everywhere convergence of Walsh-Fourier series for functions in L^2.

In Fefferman, C. Fefferman gave an alternative proof of Carleson's theorem via an a priori bound for Carleson's operator, the maximally modulated singular integral Tf(x):=\sup_{N} \int_{-\pi}^\pi e^{iNy}f(x-y)\frac 1y {dy}. In Lacey-Thiele, a duality between the approaches by Carleson and Fefferman was pointed out and a more symmetric and self-dual proof was presented.

Various strengthenings of Fefferman's estimates for Carleson's operator have appeared since, such as bounds for a higher dimensional Carleson operator in the isotropic and anisotropic setting. The supremum norm in the variable N in the displayed operator above was strengthened to maximal multiplier norms with applications to return times theorems in ergodic theory. It was strengthened to variation norms V^r with r > 2 with applications to nonlinear analysis.

Stein and Wainger proposed to study variants of the displayed operator above replacing the linear modulation phase Ny by polynomial phases in y and proved a result for polynomials without a linear term. This was generalized by Lie to general polynomial Carleson operators, first for a supremum over all quadratic polynomials and then for a supremum over all polynomials. The polynomial Carleson operator was further generalized to higher dimensions and Holder regular kernels. The development of polynomial Carleson operators has led to further generalisations, for example to almost everywhere convergence of Malmquist-Takenaka series and maximally modulated singular Radon transforms.

Surveys to Carleson's theorem can be found in the literature.

In this blueprint, we prove Theorem Theorem 1.1 as a corollary to a further generalization of the polynomial Carleson operator towards doubling metric measure spaces, Theorem Theorem 1.2 below, which is new and appears in the sibling communication. Theorem metric-space-Carleson is an axiomatic approach to Carleson type theorems on doubling metric measure spaces. This axiomatic approach is suitable for formalization and a good route towards the classical theorem.

Early drafts of the sibling communication existed in summer 2023. Based on this, the first draft of the present blueprint was written in the first half of 2024, containing a much more detailed proof, which involved increasing the size by a factor of four, and adding the derivation of Carleson's classical result. In June 2024, the fourth author launched a public website to post the blueprint, using the open-source software leanblueprint developed by Patrick Massot, calling for contributions to formalize the proof. The goal was to formalize the blueprint in the Lean proof assistant, building on top of its mathematical library Mathlib. The work was split up into about 180 tasks, to be claimed by individual contributors. Most tasks were to formalize the proof of a single lemma from the blueprint, and some were to develop basic theory or refactor existing code. The contributors adapted the blueprint to fix some gaps found during the formalization and gave feedback that led to discussions about the proof. This even resulted in a few changes to the general setup and the main theorems. All of the gaps found required only fairly localized changes to the blueprint, indicating that the initial blueprint was already of high quality. The formalization was completed in July 2025. It is attached to this arXiv posting, and the latest version can be found on GitHub.

Everyone that completed a substantial amount of tasks is included as a coauthor of the blueprint. The authors acknowledge contributions in the form of small formalization additions, pointing out corrections to the blueprint, or supplying ideas to the Lean efforts by the following people: Michel Alexis, Bolton Bailey, Julian Berman, Joachim Breitner, Martin Dvorak, Georges Gonthier, Aaron Hill, Austin Letson, Bhavik Mehta, Eric Paul, Clara Torres, Dennis Tsar, Andrew Yang, Ruben van de Velde.

Acknowledgement. L.B., M.I.d.F.F., L.D., F.v.D., M.R., R.S., and C.T. were funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany's Excellence Strategy -- EXC-2047/1 -- 390685813. L.B., R.S., and C.T. were also supported by SFB 1060. A.J. is funded by the TUBITAK (Scientific and Technological Research Council of Turkiye) under Grant Number 123F122. J.R. was supported in part by NSF grant DMS-2154835 and a HIM fellowship for the Fall 2024 trimester program in Bonn.

1.1.1. Statement of the metric space Carleson theorems🔗

Let a \ge 4 be a natural number that as it gets larger will allow for more general applications of Theorem Theorem 1.2 but will worsen the constants in the estimates.

A doubling metric measure space (X,\rho,\mu,a) is a complete and locally compact metric space (X,\rho) equipped with a non-zero locally finite Borel measure \mu that satisfies the doubling condition that for all x \in X and all R > 0 we have \mu(B(x,2R)) \le 2^a \mu(B(x,R)), where we have denoted by B(x,R) the open ball of radius R centered at x: B(x,R):=\{y\in X: \rho(x,y)<R\}. In a doubling metric measure space the closed balls are compact and \mu is positive on all non-empty open sets.

A collection \Mf of real valued continuous functions on the doubling metric measure space (X,\rho,\mu,a) is called compatible, if there is a point o\in X where all the functions are equal to 0, and if there exists for each ball B \subset X a metric d_B on \Mf, such that the following five properties are satisfied. For every ball B \subset X \sup_{x,y\in B} |\mfa(x)-\mfa(y)-\mfb(x)+\mfb(y)| \le d_B(\mfa,\mfb). For any two balls B_1=B(x_1,R), B_2=B(x_2,2R) in X with x_1\in B_2 and any \mfa,\mfb\in \Mf, d_{B_2}(\mfa,\mfb)\le 2^a d_{B_1}(\mfa,\mfb). For any two balls B_1, B_2 in X with B_1 \subset B_2 and any \mfa,\mfb\in \Mf d_{B_1}(\mfa,\mfb) \le d_{B_2}(\mfa,\mfb) and for any two balls B_1=B(x_1,R), B_2=B(x_2,2^aR) with B_1 \subset B_2, and \mfa,\mfb\in \Mf, 2d_{B_1}(\mfa,\mfb)\le d_{B_2}(\mfa,\mfb). For every ball B in X and every d_B-ball \tilde B of radius 2R in \Mf, there is a collection \mathcal{B} of at most 2^a many d_B-balls of radius R covering \tilde B, that is, \tilde B\subset \bigcup \mathcal{B}.

Further, a compatible collection \Mf is called cancellative, if for any ball B in X of radius R, any Lipschitz function \varphi: X\to \C supported on B, and any \mfa,\mfb\in \Mf we have |\int_B e(\mfa(x)-\mfb(x)) \varphi(x)\, d\mu(x)| \le 2^a \mu(B)\|\varphi\|_{\Lip(B)}(1+d_B(\mfa,\mfb))^{-1/a}, where \|\cdot\|_{\Lip(B)} denotes the inhomogeneous Lipschitz norm on B: \|\varphi\|_{\Lip(B)} = \sup_{x \in B} |\varphi(x)| + R \sup_{x,y \in B, x \neq y} \frac{|\varphi(x) - \varphi(y)|}{\rho(x,y)}.

A one-sided Calderon-Zygmund kernel K on the doubling metric measure space (X,\rho,\mu,a) is a measurable function K:X\times X\to \mathbb{C} such that for all x,y',y\in X with x\neq y, we have |K(x,y)| \le \frac{2^{a^3}}{V(x,y)} and if 2\rho(y,y') \le \rho(x,y), then |K(x,y) - K(x,y')| \le \left(\frac{\rho(y,y')}{\rho(x,y)}\right)^{1/a}\frac{2^{a^3}}{V(x,y)}, where V(x,y):=\mu(B(x,\rho(x,y))). Define the maximally truncated non-tangential singular integral T_* associated with K by T_{*}f(x):=\sup_{R_1 < R_2} \sup_{\rho(x,x')<R_1} \left|\int_{R_1< \rho(x',y) < R_2} K(x',y) f(y) \, \mathrm{d}\mu(y) \right|. We define the generalized Carleson operator T by Tf(x):=\sup_{\mfa\in\Mf} \sup_{0 < R_1 < R_2}\left| \int_{R_1 < \rho(x,y) < R_2} K(x,y) f(y) e(\mfa(y)) \, \mathrm{d}\mu(y) \right|, where e(r)=e^{ir}.

Our first main result is the following restricted weak type estimate for T in the range 1<q\le 2, which by interpolation techniques recovers L^q estimates for the open range 1<q<2.

Theorem1.2
✓L∃∀Nused by 0

Uses Theorem 1.3 and Lemma 1.13. For all integers a \ge 4 and real numbers 1<q\le 2 the following holds. Let (X,\rho,\mu,a) be a doubling metric measure space. Let \Mf be a cancellative compatible collection of functions and let K be a one-sided Calderon-Zygmund kernel on (X,\rho,\mu,a). Assume that for every bounded measurable function g on X supported on a set of finite measure we have \|T_{*}g\|_{2} \leq 2^{a^3} \|g\|_2, where T_{*} is defined above. Then for all Borel sets F and G in X and all Borel functions f:X\to \C with |f|\le \mathbf{1}_F, we have, with T defined above, \left|\int_{G} T f \, \mathrm{d}\mu\right| \leq \frac{2^{443a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}.

Lean code for Theorem1.2●1 theorem
  • theoremdefined in Carleson/MetricCarleson/Main.lean
    complete
    theorem metric_carleson.{u_1}metric_carleson.{u_1} {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 ↦ ‖f x‖) ≤ F.indicator 1)
  (hT :
    MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ 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  {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 → ℂ]
  {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)
  (hTMeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ nontangentialOperator K x1 x2) 2 2 MeasureTheory.volume
  MeasureTheory.volume ↑(C_Ts a) :
    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 ↦ nontangentialOperatornontangentialOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNRealThe maximally truncated nontangential Calderon–Zygmund operator `T_*`.  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 `μ`.  carlesonOperatorcarlesonOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNRealThe generalized Carleson operator `T`, taking values in `ℝ≥0∞`.
Use `ENNReal.toReal` to get the corresponding real number.  KX → X → ℂ fX → ℂ xX ≤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 metric_carleson.{u_1}metric_carleson.{u_1} {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 ↦ ‖f x‖) ≤ F.indicator 1)
  (hT :
    MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ 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  {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 → ℂ] {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)
  (hTMeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ nontangentialOperator K x1 x2) 2 2 MeasureTheory.volume
  MeasureTheory.volume ↑(C_Ts a) :
    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 ↦
        nontangentialOperatornontangentialOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNRealThe maximally truncated nontangential Calderon–Zygmund operator `T_*`.  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 `μ`. 
      carlesonOperatorcarlesonOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNRealThe generalized Carleson operator `T`, taking values in `ℝ≥0∞`.
Use `ENNReal.toReal` to get the corresponding real number.  KX → X → ℂ fX → ℂ xX ≤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 1.1.1

In some applications, such as the Walsh-case of Carleson's theorem, the kernel K naturally depends also on the modulation functions \mfa. The fact that we do not assume Holder-continuity of the kernel K in the first argument allows us to also capture this situation.

We now state another Theorem with a slightly weaker replacement of the assumption above. It implies the Walsh-case of Carleson's theorem. For a Borel function \tQ:X\to \Mf, and \mfa \in \Mf and x\in X define R_{\tQ}(\mfa,x)=\sup\{r>0:d_{B(x,r)}(\mfa, \tQ(x))<1\} and define further T_{\tQ}^\mfa f(x):=\sup_{R_1<R_2} \ \sup_{\rho(x,x')<R_1} \left|\int_{R_1< \rho(x',y) < \min\{R_2, R_{\tQ}(\mfa,x')\}} K(x',y) f(y) \, \mathrm{d}\mu(y) \right| Define further the linearized generalized Carleson operator T_\tQ by T_\tQ f(x):= \sup_{0 < R_1 < R_2}\left| \int_{R_1 < \rho(x,y) < R_2} K(x,y) f(y) e(\tQ(x)(y)) \, \mathrm{d}\mu(y) \right|, where again e(r)=e^{ir}.

Theorem1.3
✓L∃∀Nused by 1

Uses Lemma 1.14 and Lemma 1.13. For all integers a \ge 4 and real numbers 1<q\le 2 the following holds. Let (X,\rho,\mu,a) be a doubling metric measure space. Let \Mf be a cancellative compatible collection of functions. Let \tQ:X\to \Mf be a Borel function with finite range. Let K be a one-sided Calderon-Zygmund kernel on (X,\rho,\mu,a). Assume that for every \mfa\in \Mf and every bounded measurable function g on X supported on a set of finite measure we have \|T_{\tQ}^\mfa g\|_{2} \leq 2^{a^3} \|g\|_2, where T_{\tQ}^\mfa is defined above. Then for all Borel sets F and G in X and all Borel functions f:X\to \C with |f|\le \mathbf{1}_F, we have, with T_\tQ defined above, \left|\int_{G} T_\tQ f \, \mathrm{d}\mu\right| \le \frac{2^{443a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}.

Lean code for Theorem1.3●1 theorem
  • theoremdefined in Carleson/MetricCarleson/Linearized.lean
    complete
    theorem linearized_metric_carleson.{u_1}linearized_metric_carleson.{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)
  (hT :
    ∀ (θ : Θ X),
      MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
        MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) :
  ∫⁻ (x : X) in G, linearizedCarlesonOperator (⇑Q) K f x ≤
    ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹Theorem 1.1.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)
  (hT∀ (θ : Θ 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 `μ`.  linearizedCarlesonOperatorlinearizedCarlesonOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (Q : X → Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNRealThe linearized generalized Carleson operator `T_Q`, taking values in `ℝ≥0∞`.
Use `ENNReal.toReal` to get the corresponding real number.  (⇑QMeasureTheory.SimpleFunc X (Θ X)) KX → X → ℂ fX → ℂ xX ≤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 linearized_metric_carleson.{u_1}linearized_metric_carleson.{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)
  (hT :
    ∀ (θ : Θ X),
      MeasureTheory.HasBoundedStrongType (fun x1 x2 ↦ linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
        MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) :
  ∫⁻ (x : X) in G, linearizedCarlesonOperator (⇑Q) K f x ≤
    ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹Theorem 1.1.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)
  (hT∀ (θ : Θ 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 `μ`. 
      linearizedCarlesonOperatorlinearizedCarlesonOperator.{u_2} {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A]
  [FunctionDistances ℝ X] (Q : X → Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNRealThe linearized generalized Carleson operator `T_Q`, taking values in `ℝ≥0∞`.
Use `ENNReal.toReal` to get the corresponding real number.  (⇑QMeasureTheory.SimpleFunc X (Θ X)) KX → X → ℂ fX → ℂ
        xX ≤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 1.1.2

The value of the constant factor 2^{443a^3} in Theorems Theorem 1.2 and Theorem 1.3 is by no means sharp. One source of non-sharpness is our choice to write for readability most constants in the form 2^{na^3} for some explicit constant n.

An a posteriori byproduct of the Lean formalization of this document is that Theorems Theorem 1.2 and Theorem 1.3 remain true with 2^{44a^3} instead of 2^{443a^3}. This is obtained by changing the parameter D introduced in defineD from 2^{100a^2} to 2^{7a^2}, checking that exactly the same proof goes through, tracking the constants, and getting 2^{44a^3} in the end. This value is again by no means sharp. In the formalization we define the parameter D as 2^{\mathbb{c}a^2} and the constants in this blueprint are obtained by setting \mathbb{c} = 100.