Learning path

Each declaration appears after its prerequisites.

dach h(p) in the proof of Lemma 6.1.4 (dens₁ antichain h)
M14 The maximalFunction instance that appears in Lemma 6.1.4's proof
dach_bound Equations (6.1.34) to (6.1.37) in Lemma 6.1.4
dens1_antichain Lemma 6.1.4
C2_0_3 The constant appearing in Proposition 2.0.3
antichain_operator Proposition 2.0.3
antichain_operator' Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function
antichain_operator_le_volume Documented declaration: antichain_operator_le_volume
Antichain.tile_reach Lemma 6.3.1
Antichain.𝔄_aux Def 6.3.15
Antichain.stack_density Lemma 6.3.2
Antichain.Ep_inter_G_inter_Ip'_subset_E2 We prove inclusion 6.3.24 for every p ∈ (𝔄_aux 𝔄 ϑ N) with 𝔰 p' < 𝔰 p such that (𝓘 p : Set X) ∩ (𝓘 p') ≠ ∅
Antichain.local_antichain_density Lemma 6.3.3
Antichain.C6_3_4 The constant appearing in Lemma 6.3.4
Antichain.C6_3_4' Auxiliary constant for Lemma 6.3.4
Antichain.𝔄' The set 𝔄' defined in Lemma 6.3.4
Antichain.𝔄_min The set 𝔄_-S defined in Lemma 6.3.4
Antichain.𝓛_min The set 𝓛_{-S} defined in Lemma 6.3.4
Antichain.𝓛 The set 𝓛 defined in Lemma 6.3.4
Antichain.I_p_subset_union_L Ineq
Antichain.union_L_eq_union_I_p Ineq
Antichain.𝓛' The set 𝓛* defined in Lemma 6.3.4
Antichain.union_L'_eq_union_I_p Eq. 6.3.29
Antichain.p' p' in the blueprint
Antichain.L' The L' introduced in the proof of Lemma 6.3.4
Antichain.p'' p'' in the blueprint
Antichain.p''_mem p'' in the blueprint
Antichain.pΘ p_Θ in the blueprint
Antichain.eq_6_3_35 Eq. 6.3.35
Antichain.eq_6_3_37 Eq. 6.3.37
Antichain.ineq_6_3_36 Ineq
Antichain.ineq_6_3_38 Ineq
Antichain.volume_L'_le Ineq
Antichain.global_antichain_density Lemma 6.3.4
Antichain.p₆ p in Lemma 6.1.6
Antichain.q₆ p' in the proof of Lemma 6.1.4, the Hölder conjugate exponent of p₆
Antichain.C2_0_6_q₆_le A very involved bound needed for Lemma 6.1.4
Antichain.C6_1_6 The constant appearing in Lemma 6.1.6
Antichain.tile_count Lemma 6.1.6
tile_disjointness Lemma 6.1.1
C6_1_2 Constant appearing in Lemma 6.1.2
norm_Ks_le' Composition of inequalities 6.1.6, 6.1.7, 6.1.8
maximal_bound_antichain Lemma 6.1.2
C6_1_3 Constant appearing in Lemma 6.1.3
Lemma6_1_3.𝓜 The maximal function used in the proof of Lemma 6.1.3
Lemma6_1_3.qt $\tilde{q}$ from definition 6.1.10, as a real number
Lemma6_1_3.p Exponent used for the application of Hölder's inequality in the proof of Lemma 6.1.3
Lemma6_1_3.𝓜p The p maximal function used in the proof
Lemma6_1_3.eLpNorm_𝓜p_le Maximal function bound needed in the proof
Lemma6_1_3.eLpNorm_𝓜_le_eLpNorm_𝓜p_mul A maximal function bound via an application of H"older's inequality
Lemma6_1_3.const_check Tedious check that the constants work out
dens2_antichain Lemma 6.1.3 (inequality 6.1.11)
Tile.correlation Def 6.2.1 (from Lemma 6.2.1), denoted by φ(y) in the blueprint
Tile.mem_ball_of_correlation_ne_zero First part of Lemma 6.2.1 (eq
Tile.C6_2_1 The constant from lemma 6.2.1
Tile.e625 Ineq
Tile.correlation_kernel_bound Second part of Lemma 6.2.1 (eq
Tile.range_support Lemma 6.2.2
Tile.C6_2_3 The constant from lemma 6.2.3
Tile.uncertainty' Lemma 6.2.3 (dist version)
Tile.uncertainty Lemma 6.2.3 (edist version)
Tile.C6_1_5 The constant from lemma 6.1.5
Tile.I12 Definition (6.2.27)
Tile.I12_le' Inequality (6.2.28)
Tile.I12_le Inequality (6.2.29)
Tile.volume_coeGrid_le Inequality (6.2.32)
Tile.correlation_le_of_nonempty_inter We assume 6.2.23
Tile.correlation_le_of_empty_inter If (6.2.23) does not hold, the LHS is zero and the result follows trivially
Tile.correlation_le Part 1 of Lemma 6.1.5 (eq
Tile.correlation_zero_of_ne_subset Part 2 of Lemma 6.1.5 (claim 6.1.44)
near_1_geometric_bound A bound on the sum of a geometric series whose ratio is close to 1
summable_of_le_on_nonzero local lemma
fourierCoeffOn_bound TODO: might be generalized assumptions might be weakened, and constant given explicitely
periodic_deriv TODO: Assumptions might be weakened
fourierCoeffOn_ContDiff_two_bound TODO: might be generalized
int_sum_nat TODO : Assumptions might be weakened
fourierCoeff_eq_fourierCoeff_of_aeeq TODO: I think the measurability assumptions might be unnecessary
Function.Periodic.uniformContinuous_of_continuous TODO: maybe generalize to (hc : ContinuousOn f (Set.Icc 0 T)) and leave out condition (hT : 0 < T)
lower_secant_bound Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant
exceptional_set_carleson Theorem 1.1 (Classical Carleson)
carleson_hunt_real Carleson's theorem asserting a.e. point-wise convergence of the partial Fourier sums for periodic L^p functions, p > 1
classical_carleson_from_carleson_hunt_real Classical Carleson from the Carleson-Hunt theorem after carleson_hunt_real
carleson_hunt' Version of carleson_hunt with volume instead of haarAddMeasure in the assumption
carleson_hunt Classical theorem of Carleson and Hunt asserting a.e. convergence of the partial Fourier sums for L^p functions for p > 1
ae_tendsto_zero_of_distribution_le TODO: generalize and clean this up
Function.Periodic.ae_of_ae_restrict TODO: might be generalized
general_carlesonOperator_on_the_reals_hasStrongType Version of Lemma 11.1.5 for general exponents
rcarleson' Replacement for Lemma 11.1.5
Real.vol_real_eq remove?
Real.vol_eq proof can be simplified with enorm lemma
Real.vol_real_symm remove?
Real.vol_symm proof can be simplified with enorm lemma
carlesonOperatorReal_le_carlesonOperator TODO : change name to reflect that this only holds for a specific instance of CarlesonOperaterReal?
rcarleson_general Version of Lemma 11.1.5 for general exponents
rcarleson Lemma 11.1.5
carlesonOperatorReal TODO: avoid this extra definition?
Qᵣ Rationals as a set of real numbers
Qᵣ_dense Rationals are dense in reals
Qᵣ_countable Rationals are countable after conversion to reals, too
exceptional_set_carleson' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx Theorem 1.1 (Classical Carleson)
carleson_interval' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
classical_carleson Classical Carleson theorem after carleson_interval', exceptional_set_carleson'
C_distribution_carlesonOperatorReal_le The constant used in C_distribution_carlesonOperatorReal_le
C_control_approximation_effect The constant used in C_control_approximation_effect
control_approximation_effect This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint
ENNReal.le_on_subset TODO: might be generalized
operatorBound The function used to bound the partial Fourier sum in partialFourierSum_bound
rcarleson_exceptional_set_estimate_specific TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
rcarleson_exceptional_set_estimate_specific' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
rcarleson_exceptional_set_estimate_specific'' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
C_distribution_carlesonOperatorReal_le' The constant used in C_distribution_carlesonOperatorReal_le'
C_distribution_carlesonOperatorReal_le'_pos TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
C_distribution_carlesonOperatorReal_le'_property TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
distribution_carlesonOperatorReal_le' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
C_control_approximation_effect' The constant used in C_control_approximation_effect'
C_control_approximation_effect'_pos TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
C_control_approximation_effect'_property TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
C_control_approximation_effect'_le TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx
control_approximation_effect' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint
dirichletKernel_eq Second part of Lemma 11.1.8 (Dirichlet kernel) from the paper
dirichletKernel_eq_ae "a.e." version of previous lemma
partialFourierSum_eq_conv_dirichletKernel First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint
Function.Periodic.exists_mem_Ico₀' Adapted from mathlib Function.Periodic.exists_mem_Ico₀
Function.Periodic.exists_mem_Ico' Adapted from mathlib Function.Periodic.exists_mem_Ico₀
Hilbert_kernel_bound Lemma 11.1.11 (Hilbert kernel bound)
Hilbert_kernel_regularity_main_part Main part of the proof of Hilbert_kernel_regularity TODO: This can be local, i.e. invisible to other files
Hilbert_kernel_regularity Lemma 11.1.12 (Hilbert kernel regularity)
doublingMeasure_real_two The volume measure on the real line is doubling
modulationOperator The modulation operator M_n g, defined in (11.3.1)
approxHilbertTransform The approximate Hilbert transform L_N g, defined in (11.3.2)
niceKernel The kernel k_r(x) defined in (11.3.11)
mean_zero_oscillation Lemma 11.1.8
spectral_projection_bound Lemma 11.1.10
modulated_averaged_projection Lemma 11.3.1
young_convolution Lemma 11.3.3
integrable_bump_convolution Lemma 11.3.4
dirichletApprox The function L', defined in the Proof of Lemma 11.3.5
continuous_dirichletApprox Lemma 11.3.5, part 1
periodic_dirichletApprox Lemma 11.3.5, part 2
approxHilbertTransform_eq_dirichletApprox Lemma 11.3.5, part 3
eLpNorm_convolution_dirichletApprox The convolution with dirichletApprox is controlled on (0, 2π] in L^2 norm
dirichletApproxAux The function L'', defined in the Proof of Lemma 11.3.5
dist_dirichletApprox_le Lemma 11.3.5, part 4
norm_czOperator_le_add As the kernel of the Hilbert transform is well approximated by dirichletApprox, up to an error controlled by 12 * niceKernel r, we may bound czOperator K in terms of these
eLpNorm_czOperator_restrict_two_three_of_support_subset The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r
eLpNorm_czOperator_restrict_two_three The operator czOperator K r is bounded from L^2 [1, 4] to L^2 [2, 3], uniformly in r
eLpNorm_czOperator_restrict The operator czOperator K r is bounded from L^2 [a - 1, a + 2] to L^2 [a, a + 1], uniformly in r and a
Hilbert_strong_2_2 Lemma 11.1.6
L2norm_sq_eq TODO: move somewhere else?
partialFourierSum Partial Fourier sum
Real.vol The "volume function" V
iLipENorm The inhomogeneous Lipschitz norm on a ball
localOscillation The local oscillation of two functions w.r.t
BoundedFiniteSupport Bounded measurable function $g$ on $X$ supported on a set of finite measure
MeasureTheory.HasBoundedStrongType A weaker version of HasStrongType
MeasureTheory.Measure.IsDoubling A doubling measure is a measure on a metric space with the condition that doubling the radius of a ball only increases the volume by a constant factor, independent of the ball
MeasureTheory.DoublingMeasure A metric space with a measure with some nice properties, including a doubling condition
FunctionDistances A class stating that continuous functions have distances associated to every ball
WithFunctionDistance Class used to endow Θ X with a pseudometric space structure
CoveredByBalls s can be covered by at most N balls with radius r
BallsCoverBalls Balls of radius r in X are covered by n balls of radius r'
AllBallsCoverBalls For all r, balls of radius r in X are covered by n balls of radius a * r
CompatibleFunctions A set Θ of (continuous) functions is compatible
IsCancellative Θ is τ-cancellative
upperRadius R_Q(θ, x) defined in (1.1.17)
linearizedNontangentialOperator The linearized maximally truncated nontangential Calderon–Zygmund operator T_Q^θ
nontangentialOperator The maximally truncated nontangential Calderon–Zygmund operator T_*
carlesonOperatorIntegrand The integrand in the (linearized) Carleson operator
linearizedCarlesonOperator The linearized generalized Carleson operator T_Q, taking values in ℝ≥0∞
carlesonOperator The generalized Carleson operator after linearizedCarlesonOperator, carlesonOperatorIntegrand
defaultA This is usually the value of the argument A in DoublingMeasure and CompatibleFunctions
defaultτ defaultτ is the inverse of a
C_K The constant used twice in the definition of the Calderon-Zygmund kernel
IsOneSidedKernel K is a one-sided Calderon-Zygmund kernel
KernelProofData Standing assumptions for the kernel chapters
C1_0_2 The constant used in MetricSpaceCarleson and LinearizedMetricCarleson
C_Ts A constant used on the boundedness of T_Q^θ and T_*
ClassicalCarleson Carleson's theorem (statement) after partialFourierSum
MetricSpaceCarleson Metric space Carleson theorem (statement) after KernelProofData, carlesonOperator, nontangentialOperator, C1_0_2
LinearizedMetricCarleson Theorem 1.1.2
𝓒 The partition 𝓒(G, k) of Grid X by volume, given in (5.1.1) and (5.1.2)
TilesAt The definition 𝔓(k) given in (5.1.3)
𝔐 The definition 𝔐(k, n) given in (5.1.4) and (5.1.5)
dens' The definition dens'_k(𝔓') given in (5.1.6)
ℭ The partition ℭ(k, n) of 𝔓(k) by density, given in (5.1.7)
dens1_le_dens' Lemma 5.3.11
dens1_le Lemma 5.3.12
𝔅 The subset 𝔅(p) of 𝔐(k, n), given in (5.1.8)
ℭ₁ The subset ℭ₁(k, n, j) of ℭ(k, n), given in (5.1.9)
𝔏₀ The subset 𝔏₀(k, n) of ℭ(k, n), given in (5.1.10)
𝔏₁ 𝔏₁(k, n, j, l) consists of the minimal elements in ℭ₁(k, n, j) not in 𝔏₁(k, n, j, l') for some l' < l
ℭ₂ The subset ℭ₂(k, n, j) of ℭ₁(k, n, j), given in (5.1.13)
𝔘₁ The subset 𝔘₁(k, n, j) of ℭ₁(k, n, j), given in (5.1.14)
𝔏₂ The subset 𝔏₂(k, n, j) of ℭ₂(k, n, j), given in (5.1.15)
ℭ₃ The subset ℭ₃(k, n, j) of ℭ₂(k, n, j), given in (5.1.16)
𝔏₃ 𝔏₃(k, n, j, l) consists of the maximal elements in ℭ₃(k, n, j) not in 𝔏₃(k, n, j, l') for some l' < l
ℭ₄ The subset ℭ₄(k, n, j) of ℭ₃(k, n, j), given in (5.1.19)
𝓛 The subset 𝓛(u) of Grid X, given near (5.1.20)
𝔏₄ The subset 𝔏₄(k, n, j) of ℭ₄(k, n, j), given near (5.1.22)
ℭ₅ The subset ℭ₅(k, n, j) of ℭ₄(k, n, j), given in (5.1.23)
highDensityTiles The set $\mathcal{P}_{F,G}$, defined in (5.1.24)
G₁ The exceptional set G₁, defined in (5.1.25)
setA The set A(λ, k, n), defined in (5.1.26)
MsetA Finset of cubes in setA
G₂ The set G₂, defined in (5.1.27)
G₃ The set G₃, defined in (5.1.28)
G' The set G', defined below (5.1.28)
𝔓₁ The set 𝔓₁, defined in (5.1.30)
C5_2_9 The constant in Lemma 5.2.9, with value D ^ (1 - κ * Z * (n + 1))
third_exception_rearrangement A rearrangement for Lemma 5.2.9 that does not require the tile structure
first_exception' Lemma 5.2.1
dense_cover Lemma 5.2.2
pairwiseDisjoint_E1 Lemma 5.2.3
dyadic_union Lemma 5.2.4
john_nirenberg_aux1 Equation (5.2.7) in the proof of Lemma 5.2.5
john_nirenberg_aux2 Equation (5.2.11) in the proof of Lemma 5.2.5
john_nirenberg Lemma 5.2.5
second_exception Lemma 5.2.6
layervol The volume of a "layer" in the key function of Lemma 5.2.7
top_tiles Lemma 5.2.7
𝔘 The function 𝔘(m) used in the proof of Lemma 5.2.8
big_ball Ball that covers the image of 𝒬
tree_count Lemma 5.2.8
boundary_exception Lemma 5.2.9
third_exception Lemma 5.2.10
exceptional_set Lemma 5.1.1
𝔓pos The set 𝔓_{G\G'} in the blueprint
ℜ₀ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₀
ℜ₁ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁
ℜ₂ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂
ℜ₃ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃
mem_iUnion_iff_mem_of_mem_ℭ Lemma allowing to peel ⋃ (n : ℕ) (k ≤ n) from unions in the proof of Lemma 5.5.1
mem_iUnion_iff_mem_of_mem_ℭ₁ Lemma allowing to peel ⋃ (j ≤ 2 * n + 3) from unions in the proof of Lemma 5.5.1
antichain_decomposition Lemma 5.5.1
𝔏₀' The subset 𝔏₀(k, n, l) of 𝔏₀(k, n), given in Lemma 5.5.3
ceil_log2_le_floor_four_add_log2 Logarithmic inequality used in the proof of Lemma 5.5.2
𝔒 The set 𝔒 in the proof of Lemma 5.5.2
iUnion_L0' Main part of Lemma 5.5.2
pairwiseDisjoint_L0' Part of Lemma 5.5.2
antichain_L0' Part of Lemma 5.5.2
ℭ₁' Type synonym of ℭ₁ to apply the Preorder of the proof of Lemma 5.5.3 on
antichain_L2 Lemma 5.5.3
antichain_L1 Part of Lemma 5.5.4
antichain_L3 Part of Lemma 5.5.4
carlesonSum_𝔓₁_compl_eq_𝔓pos_inter The Carleson sum over 𝔓₁ᶜ and 𝔓pos ∩ 𝔓₁ᶜ coincide at ae every point of G \ G'
carlesonSum_𝔓pos_eq_sum The Carleson sum over 𝔓pos ∩ 𝔓₁ᶜ can be decomposed as a sum over the intersections of this set with various ℭ k n
carlesonSum_𝔓pos_inter_ℭ_eq_add_sum In each set ℭ k n, the Carleson sum can be decomposed as a sum over 𝔏₀ k n and over various ℭ₁ k n j
carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum In each set ℭ₁ k n j, the Carleson sum can be decomposed as a sum over ℭ₂ k n j and over various 𝔏₁ k n j l
carlesonSum_𝔓pos_inter_ℭ₂_eq_add_sum In each set ℭ₂ k n j, the Carleson sum can be decomposed as a sum over 𝔏₂ k n j and over various 𝔏₃ k n j l
lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral Documented declaration: lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral
lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ Custom version of the antichain operator theorem, in the specific form we need to handle the various terms in the previous statement
C5_1_3_optimized An optimized constant for Lemma 5.1.3
C5_1_3 The constant used in Lemma 5.1.3
forest_complement Lemma 5.1.3, proving the bound on the integral of the Carleson sum over all leftover tiles which do not fit in a forest
ordConnected_tilesAt Lemma 5.3.4
ordConnected_C Lemma 5.3.5
ordConnected_C1 Lemma 5.3.6
ordConnected_C2 Lemma 5.3.7
ordConnected_C3 Lemma 5.3.8
ordConnected_C4 Lemma 5.3.9
ordConnected_C5 Lemma 5.3.10
ℭ₆ The subset ℭ₆(k, n, j) of ℭ₅(k, n, j), given above (5.4.1)
𝔗₁ The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1)
𝔘₂ The subset 𝔘₂(k, n, j) of 𝔘₁(k, n, j), given in (5.4.2)
URel The relation ∼ defined below (5.4.2)
URel.not_disjoint Lemma 5.4.1, part 2
URel.eq Lemma 5.4.1, part 1
urel_of_not_disjoint Helper for 5.4.2 that is also used in 5.4.9
equivalenceOn_urel Lemma 5.4.2
𝔘₃ 𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j, given above (5.4.5)
𝔗₂ The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5)
C6_forest Lemma 5.4.3
forest_disjoint This one could deserve a lemma in the blueprint, as it is needed to decompose the sum of Carleson operators over disjoint subfamilies
forest_geometry Lemma 5.4.4, verifying (2.0.32)
forest_convex Lemma 5.4.5, verifying (2.0.33)
forest_separation Lemma 5.4.6, verifying (2.0.36) Note: swapped u and u' to match (2.0.36)
forest_inner Lemma 5.4.7, verifying (2.0.37)
C5_4_8 The multiplicity appearing in Lemma 5.4.8
mf The good choice of an element to get a contradiction in the proof of Lemma 5.4.8
forest_stacking Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34
𝔘₄ Define 𝔘₄ k n j l as the union of 2 ^ n disjoint subfamilies in 𝔘₃ k n j, to make sure the multiplicity is at most 2 ^ n to get a forest
iUnion_𝔘₄ The sets (𝔘₄(k, n, j, l))_l form a partition of 𝔘₃ k n j
forest The forest based on 𝔘₄ k n j l
carlesonSum_𝔓₁_eq_sum From the fact that the ℭ₅ k n j are disjoint, one can rewrite the whole Carleson sum over 𝔓₁ (the union of the ℭ₅ k n j) as a sum of Carleson sums over the ℭ₅ k n j
carlesonSum_ℭ₅_eq_ℭ₆ The Carleson sum over ℭ₅ and ℭ₆ coincide, for points in G \ G'
carlesonSum_ℭ₆_eq_sum The Carleson sum over ℭ₆ can be decomposed as a sum over 4 n + 12 forests based on 𝔘₄ k n j l
lintegral_carlesonSum_forest For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁
lintegral_carlesonSum_forest' For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁
forest_union_aux Putting all the above decompositions together, one obtains a control of the integral of the full Carleson sum over 𝔓₁, as a sum over all the forests
C5_1_2_optimized An optimized constant for the forest union theorem
forest_union_optimized Version of the forest union result with a better constant
C5_1_2 The constant used in Lemma 5.1.2
forest_union Documented declaration: forest_union
C2_0_2 The constant used in Proposition 2.0.2
defaultD The constant D from (2.0.1)
nnD D as an element of ℝ≥0
defaultκ The constant κ from (2.0.2)
defaultZ The constant Z from (2.0.3)
hundred_lt_D used in 7.5.6 (limited_scale_impact)
hundred_lt_realD used in 7.5.6 (limited_scale_impact)
twentyfive_le_realD used in 4.1.7 (small_boundary)
eight_le_realD used in 4.1.3 (I3_prop_3_1)
five_le_realD used in 4.1.6 (transitive_boundary)
four_le_realD used in various places in Carleson.TileExistence
nnτ τ as an element of ℝ≥0
MeasureTheory.DoublingMeasure.mono Monotonicity of doubling measure metric spaces in A
cancelPt The point o in the blueprint
isCancellative_of_norm_integral_exp_le Constructor of IsCancellative in terms of real norms instead of extended reals
vol The "volume function" V
𝔓X_s Used to simplify notation in the proof of tile_sum_operator
tile_sum_operator Lemma 4.0.3
C2_0_1 The constant used in Proposition 2.0.1
finitary_carleson Proposition 2.0.1
TileStructure.Forest An n-forest
TileStructure.Row An n-row
TileStructure.Forest.adjointBoundaryOperator The operator S_{2,𝔲} f(x), given above Lemma 7.4.3
TileStructure.Forest.𝔖₀ The set 𝔖 defined in the proof of Lemma 7.4.4
TileStructure.Forest.adjoint_tile_support1 Part 1 of Lemma 7.4.1
TileStructure.Forest.adjoint_tile_support2 Part 2 of Lemma 7.4.1
TileStructure.Forest.adjoint_tile_support2_sum_partial A partially applied variant of adjoint_tile_support2_sum, used to prove Lemma 7.7.3
TileStructure.Forest.adjoint_tree_estimate Part 1 of Lemma 7.4.2
TileStructure.Forest.indicator_adjoint_tree_estimate Part 2 of Lemma 7.4.2
TileStructure.Forest.adjoint_tree_control Lemma 7.4.3
TileStructure.Forest.overlap_implies_distance Part 1 of Lemma 7.4.7
TileStructure.Forest.𝔗_subset_𝔖₀ Part 2 of Lemma 7.4.7
TileStructure.Forest.correlation_separated_trees Lemma 7.4.4
TileStructure.Forest.rowDecomp The row-decomposition of a tree, defined in the proof of Lemma 7.7.1
TileStructure.Forest.biUnion_rowDecomp Part of Lemma 7.7.1
TileStructure.Forest.pairwiseDisjoint_rowDecomp Part of Lemma 7.7.1
TileStructure.Forest.carlesonRowSum The definition of T_{ℜ_j}f(x), defined above Lemma 7.7.2
TileStructure.Forest.adjointCarlesonRowSum The definition of T_{ℜ_j}*f(x), defined above Lemma 7.7.2
TileStructure.Forest.adjointCarlesonRowSum_adjoint adjointCarlesonRowSum is the adjoint of carlesonRowSum
TileStructure.Forest.row_bound_common Common proof structure for the two parts of Lemma 7.7.2
TileStructure.Forest.row_correlation Lemma 7.7.3
TileStructure.Forest.rowSupport The definition of Eⱼ defined above Lemma 7.7.4
TileStructure.Forest.pairwiseDisjoint_rowSupport Lemma 7.7.4
TileStructure.Forest.G2_0_4 The constant on the g side of Proposition 2.0.4
TileStructure.Forest.forest_operator_g The g side of Proposition 2.0.4
TileStructure.Forest.forest_operator_f_inner https://leanprover.zulipchat.com/#narrow/channel/442935-Carleson/topic/Problems.20in.20the.20forest.20operator.20proposition/near/522771057
TileStructure.Forest.C2_0_4_aux The constant in the f side of Proposition 2.0.4
TileStructure.Forest.forest_operator_f The f side of Proposition 2.0.4
forest_operator' Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function
forest_operator_le_volume Documented declaration: forest_operator_le_volume
K' Truncated version of K used in proof of nontangential_pointwise_bound
annulus_integral_bound Documented declaration: annulus_integral_bound
TileStructure.Forest.nontangential_integral_bound₂ Bound for (7.2.4) and (7.2.5) in the proof of nontangential_pointwise_bound
TileStructure.Forest.nontangential_pointwise_bound Pointwise bound needed for Lemma 7.2.2
TileStructure.Forest.nontangential_operator_bound Lemma 7.2.2
TileStructure.Forest.kissing The set of cubes in Lemma 7.2.4
TileStructure.Forest.boundary_overlap Lemma 7.2.4
TileStructure.Forest.e728 Equation (7.2.8) in the proof of Lemma 7.2.3
TileStructure.Forest.boundary_geometric_series Bound for the inner sum in Equation (7.2.8)
TileStructure.Forest.boundary_operator_bound Lemma 7.2.3
TileStructure.Forest.eI𝒬u_mul Auxiliary function used in the proof of Lemma 7.2.1
TileStructure.Forest.le_C7_2_1 The natural constant for Lemma 7.2.1 is ≤ the simpler constant C7_2_1 we use instead
TileStructure.Forest.eLpNorm_two_cS_bound_le Main estimate used in the proof of tree_projection_estimate
TileStructure.Forest.Complex.enorm_real TODO: PR next to Complex.norm_real
TileStructure.Forest.tree_projection_estimate Lemma 7.2.1
TileStructure.Forest.𝓙₅ The definition 𝓙' at the start of Section 7.5.1
TileStructure.Forest.χtilde The definition of χ-tilde, defined in the proof of Lemma 7.5.2
TileStructure.Forest.χ The definition of χ, defined in the proof of Lemma 7.5.2
TileStructure.Forest.holderFunction The definition of h_J, defined in the proof of Section 7.5.2
TileStructure.Forest.union_𝓙₅ Part of Lemma 7.5.1
TileStructure.Forest.pairwiseDisjoint_𝓙₅ Part of Lemma 7.5.1
TileStructure.Forest.moderate_scale_change Lemma 7.5.3 (stated somewhat differently)
TileStructure.Forest.sum_χ Part of Lemma 7.5.2
TileStructure.Forest.χ_le_indicator Part of Lemma 7.5.2
TileStructure.Forest.dist_χ_le Part of Lemma 7.5.2
TileStructure.Forest.holder_correlation_rearrange Sub-equations (7.5.10) and (7.5.11) in Lemma 7.5.5
TileStructure.Forest.holder_correlation_tile Lemma 7.5.5
TileStructure.Forest.limited_scale_impact_first_estimate Part of Lemma 7.5.6
TileStructure.Forest.limited_scale_impact_second_estimate Part of Lemma 7.5.6
TileStructure.Forest.limited_scale_impact Lemma 7.5.6
TileStructure.Forest.local_tree_control Lemma 7.5.7
TileStructure.Forest.scales_impacting_interval Lemma 7.5.8
TileStructure.Forest.global_tree_control1_edist_part1 Part 1 of equation (7.5.18) of Lemma 7.5.9
TileStructure.Forest.global_tree_control1_edist_part2 Part 2 of equation (7.5.18) of Lemma 7.5.9
TileStructure.Forest.global_tree_control1_edist_left Equation (7.5.18) of Lemma 7.5.9 for ℭ = t u₁
TileStructure.Forest.global_tree_control1_edist_right Equation (7.5.18) of Lemma 7.5.9 for ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂
TileStructure.Forest.global_tree_control1_supbound Equation (7.5.17) of Lemma 7.5.9
TileStructure.Forest.global_tree_control2 Lemma 7.5.10
TileStructure.Forest.P7_5_4 The product on the right-hand side of Lemma 7.5.4
TileStructure.Forest.support_holderFunction_subset The support of holderFunction is in 𝓘 u₁
TileStructure.Forest.I7_5_4 An intermediate constant in Lemma 7.5.4
TileStructure.Forest.holder_correlation_tree Lemma 7.5.4
TileStructure.Forest.C7_5_11_binomial_bound A binomial bound used in Lemma 7.4.5
TileStructure.Forest.lower_oscillation_bound Lemma 7.5.11
TileStructure.Forest.correlation_distant_tree_parts Lemma 7.4.5
TileStructure.Forest.σ The definition σ(u, x) given in Section 7.1
TileStructure.Forest.𝓙₀ The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2
TileStructure.Forest.𝓙 The definition of `𝓙(𝔖), defined above Lemma 7.1.2
TileStructure.Forest.𝓛₀ The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2
TileStructure.Forest.𝓛 The definition of `𝓛(𝔖), defined above Lemma 7.1.2
TileStructure.Forest.approxOnCube The projection operator P_𝓒 f(x), given above Lemma 7.1.3
TileStructure.Forest.lintegral_eq_lintegral_approxOnCube Used in the proof of Lemma 7.1.6
TileStructure.Forest.cubeOf The definition I_i(x), given above Lemma 7.1.3
TileStructure.Forest.nontangentialMaximalFunction The definition T_𝓝^θ f(x), given in (7.1.3)
TileStructure.Forest.ijIntegral Scaled integral appearing in the definition of boundaryOperator
TileStructure.Forest.boundaryOperator The operator S_{1,𝔲} f(x), given in (7.1.4)
TileStructure.Forest.𝓑 The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3
TileStructure.Forest.c𝓑 The center function for the collection of balls 𝓑
TileStructure.Forest.r𝓑 The radius function for the collection of balls 𝓑
TileStructure.Forest.convex_scales Lemma 7.1.1, freely translated
TileStructure.Forest.biUnion_𝓙 Part of Lemma 7.1.2
TileStructure.Forest.biUnion_𝓛 Part of Lemma 7.1.2
TileStructure.Forest.pairwiseDisjoint_𝓛 Part of Lemma 7.1.2
TileStructure.Forest.exp_Lipschitz Used in the proof of exp_sub_one_le, which is used to prove Lemma 7.1.4
TileStructure.Forest.exp_sub_one_le Used in the proof of Lemma 7.1.4
TileStructure.Forest.dist_lt_5 Used in the proofs of Lemmas 7.1.4 and 7.1.5
TileStructure.Forest.L7_1_4_bound The bound in the third display in the proof of Lemma 7.1.4
TileStructure.Forest.sum_pow_two_le The geometric sum used to prove L7_1_4_sum
TileStructure.Forest.L7_1_4_sum The sum used in the proof of Lemma 7.1.4
TileStructure.Forest.L7_1_4_dist_le Inequality used twice in the proof of Lemma 7.1.4
TileStructure.Forest.s_le_s Inequality needed for the proof of L7_1_4_integral_le_integral
TileStructure.Forest.L7_1_4_integral_le_integral The integral bound needed for the proof of Lemma 7.1.4
TileStructure.Forest.L7_1_4_laverage_le_MB An average over ball (𝔠 p) (16 * D ^ 𝔰 p) is bounded by MB; needed for Lemma 7.1.4
TileStructure.Forest.first_tree_pointwise Lemma 7.1.4
TileStructure.Forest.second_tree_pointwise Lemma 7.1.5
TileStructure.Forest.L7_1_6_integral_eq Equation 7.1.10 from the blueprint
TileStructure.Forest.L7_1_6_integral_le Integral norm bound used implicitly in the third display of the proof of Lemma 7.1.6
TileStructure.Forest.L7_1_6_I_le Prove an upper bound for the function I used in the proof of Lemma 7.1.6
TileStructure.Forest.third_tree_pointwise Lemma 7.1.6
TileStructure.Forest.pointwise_tree_estimate Lemma 7.1.3
TileStructure.Forest.local_dens1_tree_bound_exists Part 1 of Lemma 7.3.2
TileStructure.Forest.local_dens1_tree_bound Lemma 7.3.2
TileStructure.Forest.local_dens2_tree_bound_aux Auxiliary result used to prove local_dens2_tree_bound
TileStructure.Forest.local_dens2_tree_bound_aux' Special case of local_dens2_tree_bound_aux which is used twice
TileStructure.Forest.local_dens2_tree_bound Lemma 7.3.3
TileStructure.Forest.eLpNorm_approxOnCube_two_le Main bound in the proof of Lemma 7.3.1
TileStructure.Forest.density_tree_bound_aux Generalization that implies both parts of Lemma 7.3.1
TileStructure.Forest.density_tree_bound1 First part of Lemma 7.3.1
TileStructure.Forest.density_tree_bound2 Second part of Lemma 7.3.1
_root_.MeasureTheory.BoundedCompactSupport.const_smul TODO: move somewhere else
smul_le_indicator rename, move somewhere else
TileStructure.Forest.𝓙₆ The definition 𝓙' at the start of Section 7.6
TileStructure.Forest.union_𝓙₆ Part of Lemma 7.6.1
TileStructure.Forest.pairwiseDisjoint_𝓙₆ Part of Lemma 7.6.1
TileStructure.Forest.thin_scale_impact_prelims Some preliminary relations for Lemma 7.6.3
TileStructure.Forest.thin_scale_impact_key The key relation of Lemma 7.6.3, which will eventually be shown to lead to a contradiction
TileStructure.Forest.thin_scale_impact Lemma 7.6.3
TileStructure.Forest.thin_scale_impact' Lemma 7.6.3 with a floor on the constant to avoid casting
TileStructure.Forest.square_function_count Lemma 7.6.4
TileStructure.Forest.e763 Equation (7.6.3) of Lemma 7.6.2
TileStructure.Forest.btp_integral_bound The critical bound on the integral in Equation (7.6.3)
TileStructure.Forest.e764_preCS Equation (7.6.4) of Lemma 7.6.2 (before applying Cauchy–Schwarz)
TileStructure.Forest.e764_postCS Equation (7.6.4) of Lemma 7.6.2 (after applying Cauchy–Schwarz and simplification)
TileStructure.Forest.bound_for_tree_projection Lemma 7.6.2
TileStructure.Forest.correlation_near_tree_parts Lemma 7.4.6
GridStructure A grid structure on X
Grid The indexing type of the grid structure
Grid.mem_def not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas
Grid.le_def not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas
Grid.int The set I ↦ Iᵒ in the blueprint
Grid.opSize An auxiliary measure used in the well-foundedness of Ω in Lemma tile_structure
Grid.exists_unique_succ There exists a unique successor of each non-maximal cube
Grid.succ If i is not a maximal element, this is the (unique) minimal element greater than i
Grid._root_.C2_1_2 The constant appearing in Lemma 2.1.2, 2 ^ {-95a}
Grid.dist_strictMono Stronger version of Lemma 2.1.2
Grid.dist_mono Weaker version of Lemma 2.1.2
Grid.dist_strictMono_iterate' Version of dist_strictMono_iterate with d in ℤ
iHolENorm the L^∞-normalized t-Hölder norm
iHolNNNorm The NNReal version of the L^∞-normalized t-Hölder norm, iHolENorm
cutoff cutoff R t x y is L(x, y) in the proof of Lemma 8.0.1
cutoff_measurable cutoff R t x is measurable in y
leq_of_max_neq_left Is this useful for mathlib?
aux_8_0_4 Equation 8.0.4 from the blueprint
C8_0_1 The constant occurring in Lemma 8.0.1
holderApprox φ ↦ \tilde{φ} in the proof of Lemma 8.0.1
support_holderApprox_subset Part of Lemma 8.0.1
dist_holderApprox_le Part of Lemma 8.0.1: Equation (8.0.1)
holderApprox_le Part of Lemma 8.0.1: sup norm control in Equation (8.0.2)
norm_holderApprox_sub_le_aux Auxiliary lemma: part of the Lipschitz control in Equation (8.0.2), when the distance between the points is at most R
norm_holderApprox_sub_le Part of Lemma 8.0.1: Lipschitz norm control in Equation (8.0.2)
C2_0_5 The constant occurring in Proposition 2.0.5
holder_van_der_corput Proposition 2.0.5
iLipNNNorm The NNReal version of the inhomogeneous Lipschitz norm on a ball, iLipENorm
rightContinuous_integral_annulus Let f be integrable over an annulus with fixed radii R₁, R₂
leftContinuous_integral_annulus Let f be integrable over an annulus with fixed radii R₁, R₂
integrableOn_coi_inner_annulus' The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus
integrableOn_coi_inner_annulus₀ The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus
integrableOn_coi_inner_annulus The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus
exists_rat_near_carlesonOperatorIntegrand' Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε
exists_rat_near_carlesonOperatorIntegrand Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε
enorm_carlesonOperatorIntegrand_le not sure if this is the best phrasing
carlesonOperator_measurable TODO: get rid of the countability assumption
linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator TODO: this proof is a good target for automation
lcoConvergent A monotone sequence of functions converging to linearizedCarlesonOperator
Θ' A countable dense subset of Θ X
J102 A countable dense subset of the range of R₁ and R₂
carlesonOperator_eq_biSup_Θ'_J102
enumΘ' An enumeration of Θ' X, assuming it is nonempty
enumΘ'ArgMax The argmax of g (enumΘ' nΘ' i) x over i ≤ n with lower indices winning ties
enumΘ'ArgMax_eq_iff The characterising property of enumΘ'ArgMax
QΘ' The simple function corresponding to the blueprint's Q_n
metric_carleson' Theorem 1.1.1, with an explicit value for the constant, corresponding to 𝕔 = 100 and following the blueprint
T_S The operator T_{s₁, s₂} introduced in Lemma 3.0.3
T_lin The operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4
CP304 Convenience structure for the parameters that stay constant throughout the recursive calls to finitary Carleson in the proof of Lemma 3.0.4
P304 All the parameters needed to apply the recursion of Lemma 3.0.4
P304.succ Construct G_{n+1} given G_n
slice slice CP bG mG n contains G_n and its associated data
exists_volume_slice_lt_eps The sets G_n become arbitrarily small
slice_integral_bound_sum The slightly unusual way of writing the integrand is to facilitate applying the monotone convergence theorem
C3_0_4 The constant used in linearized_truncation and S_truncation
linearized_truncation Lemma 3.0.4
S_truncation Lemma 3.0.3
L302 The largest integer s₁ satisfying D ^ (-(s₁ - 2)) * R₁ > 1 / 2
U302 The smallest integer s₂ satisfying D ^ (-(s₂ + 2)) * R₂ < 1 / (4 * D)
exists_uniform_annulus_bound There exists a uniform bound for all possible values of L302 and U302 over the annulus in R_truncation
edgeScales The fringes of the scale interval in Lemma 3.0.2's proof that require separate handling
T_R The operator T_{R₁, R₂, R} introduced in Lemma 3.0.2
R_truncation Lemma 3.0.2
linearized_metric_carleson Linearized metric Carleson theorem (Theorem 1.1.2) after lcoConvergent, R_truncation
metric_carleson Metric Carleson theorem (Theorem 1.1.1) after carlesonOperator_eq_biSup_Θ'_J102, linearized_metric_carleson
carlesonOn The operator T_𝔭 defined in Proposition 2.0.2
measurable_carlesonOn Documented declaration: measurable_carlesonOn
carlesonSum The operator T_ℭ f defined at the bottom of Section 7.4
adjointCarleson The definition of Tₚ*g(x), defined above Lemma 7.4.1
adjointCarlesonSum The definition of T_ℭ*g(x), defined at the bottom of Section 7.4
adjointCarlesonSum_inter A helper lemma used in Lemma 7.5.10
MKD MKD is short for "modulated kernel times dilated bump"
adjointCarleson_adjoint adjointCarleson is the adjoint of carlesonOn
adjointCarlesonSum_adjoint adjointCarlesonSum is the adjoint of carlesonSum
ProofData Data common through most of chapters 2-7 (except 3)
inv_q_mem_Ico Note: For exponent computations it is usually cleaner to argue in terms of q⁻¹ rather than q, both on paper and in Lean
nnq q as an element of ℝ≥0
two_le_κZ Used in third_exception (Lemma 5.2.10)
DκZ_le_two_rpow_100 Used in third_exception (Lemma 5.2.10)
ψ The function ψ used as a basis for a dyadic partition of unity
lipschitzWith_ψ' Alternate version of lipschitzWith_ψ that avoids using ENNReal
nonzeroS the one or two numbers s where ψ (D ^ (-s) * x) is possibly nonzero
eq_endpoints If D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x), then the endpoints of nonzeroS x are equal
endpoint_sub_one If D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x), then the endpoints of nonzeroS x differ by 1
sum_ψ₁ Special case of sum_ψ, for the case where nonzeroS D x has one element
sum_ψ₂ Special case of sum_ψ, for the case where nonzeroS D x has two elements
sum_ψ See finsum_ψ for the version that doesn't explicitly restrict to the support
Ks K_s in the blueprint
dist_mem_Icc_of_Ks_ne_zero Lemma 2.1.3 part 1, equation (2.1.2)
C2_1_3 The constant appearing in part 2 of Lemma 2.1.3
D2_1_3 The constant appearing in part 3 of Lemma 2.1.3
kernel_bound Equation (1.1.11) in the blueprint
DoublingMeasure.volume_real_ball_two_le_same_repeat Apply volume_ball_two_le_same n times
DoublingMeasure.volume_real_ball_two_le_same_repeat' Special case of DoublingMeasure.volume_ball_two_le_same_repeat used to prove div_vol_le
DoublingMeasure.volume_ball_two_le_same_repeat Apply volume_ball_two_le_same n times
DoublingMeasure.volume_ball_two_le_same_repeat' Special case of DoublingMeasure.volume_ball_two_le_same_repeat used to prove div_vol_le'
div_vol_le₀ Useful special case of div_vol_le
norm_K_le preferably use enorm_K_le
norm_Ks_le Lemma 2.1.3 part 2 (Real version)
enorm_Ks_le Lemma 2.1.3 part 2, equation (2.1.3)
enorm_Ks_le' Needed for Lemma 7.5.5
norm_Ks_le_of_dist_le Ks is bounded uniformly in x, y assuming x is in a fixed closed ball
_root_.Bornology.IsBounded.exists_bound_of_norm_Ks ‖Ks x y‖ is bounded if x is in a bounded set
enorm_ψ_sub_ψ_le_two Needed to prove ψ_ineq
enorm_Ks_sub_Ks_le_close Second case of norm_Ks_sub_Ks_le in blueprint
enorm_Ks_sub_Ks_le_far First case of norm_Ks_sub_Ks_le in blueprint
enorm_Ks_sub_Ks_le Lemma 2.1.3 part 3, equation (2.1.4)
integrable_Ks_x The function y ↦ Ks s x y is integrable
Yk_finite not sure if we actually need this; just countability seems quite good enough
aux Auxiliary lemma used in subsequent mutual blocks
cover_by_cubes the additional argument hk to get decent equality theorems
C4_1_7 TODO: fix overlapping instance warning; this will also fix the linter
const_n TODO: linter false positive
grid_existence Proof that there exists a grid structure
C𝓩 The constant appearing in 4.2.2 (3 / 10)
𝓩 A finset of maximal cardinality satisfying (4.2.1) and (4.2.2)
C4_2_1 7 / 10
frequency_ball_cover Equation (4.2.3), Lemma 4.2.1
Construction.disjoint_frequency_cubes Lemma 4.2.2
Construction.ball_subset_Ω₁ Equation (4.2.6), first inclusion
Construction.Ω₁_subset_ball Equation (4.2.6), second inclusion
Construction.iUnion_ball_subset_iUnion_Ω₁ Equation (4.2.5)
Construction.CΩ 1 / 5
PreTileStructure The data in a tile structure, and some basic properties
TileStructure A tile structure
volume_xDsp_bound A bound used in both nontrivial cases of Lemma 7.5.5
volume_xDsp_bound_4 A bound used in Lemma 7.6.2
E The set E defined in Proposition 2.0.2
smul This is not defined as such in the blueprint, but λp ≲ λ'p' can be written using smul l p ≤ smul l' p'
tile_le_of_cube_le_and_not_disjoint Deduce an inclusion of tiles from an inclusion of their cubes and non-disjointness of their Ωs
smul_mono Lemma 5.3.1
smul_C2_1_2 Lemma 5.3.2 (generalizing 1 to k > 0)
C5_3_3 The constraint on λ in the first part of Lemma 5.3.3
wiggle_order_11_10 Lemma 5.3.3, Equation (5.3.3)
wiggle_order_100 Lemma 5.3.3, Equation (5.3.4)
wiggle_order_500 Lemma 5.3.3, Equation (5.3.5)
TileLike.toSet From a TileLike, we can construct a set
lowerCubes 𝔓(𝔓') in the blueprint
dens₁ This density is defined to live in ℝ≥0∞
dens₂ This density is defined to live in ℝ≥0∞
dens₁_le_one A rough estimate
stackSize The number of tiles p in s whose underlying cube 𝓘 p contains x
stackSize_real Simplify the cast of stackSize C x from ℕ to ℝ
exists_maximal_disjoint_covering_subfamily Given any family of tiles, one can extract a maximal disjoint subfamily, covering everything
maximalSubfamily A disjoint subfamily of A covering everything
iteratedMaximalSubfamily Iterating maximalSubfamily to obtain disjoint subfamilies of A
eq_biUnion_iteratedMaximalSubfamily Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size
MeasureTheory.convolution_symm Special case of convolution_flip when L is symmetric
MeasureTheory.AEStronglyMeasurable.convolution The convolution of two a.e. strongly measurable functions is a.e. strongly measurable
MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm This implies both of the following theorems convolutionExists_of_memLp_memLp and enorm_convolution_le_eLpNorm_mul_eLpNorm
MeasureTheory.ConvolutionExists.of_memLp_memLp If MemLp f p μ and MemLp g q μ, where p and q are Hölder conjugates, then the convolution of f and g exists everywhere
MeasureTheory.enorm_convolution_le_eLpNorm_mul_eLpNorm If p and q are Hölder conjugates, then the convolution of f and g is bounded everywhere by eLpNorm f p μ * eLpNorm g q μ
RCLike.Components TODO: check whether this is the right approach
RCLike.component TODO: check whether this is the right approach
RCLike.norm_realPart_le Norm of the real component part is at most ‖a‖
RCLike.norm_imPart_le Norm of the imaginary component part is at most ‖a‖
RCLike.norm_posReal_le max(re a, 0) embedded in 𝕂 has norm at most |re a|
RCLike.norm_negReal_le max(-re a, 0) negated and embedded in 𝕂 has norm at most |re a|
RCLike.norm_posIm_le I * max(im a, 0) has norm at most ‖I * im⁺ - I * im⁻‖
RCLike.norm_negIm_le -I * max(-im a, 0) has norm at most ‖I * im⁺ - I * im⁻‖
RCLike.induction TODO: clean up the proof
Set.Annulus.oc Set.Annulus.oo has moved to Defs.lean
Set.Annulus.biUnion_Ici_co_map_succ Union formula for Set.Annulus.co x (f i) (f (Order.succ i)) over i ∈ Ici a
Set.Annulus.biUnion_Ici_oc_map_succ Union formula for Set.Annulus.oc x (f i) (f (Order.succ i)) over i ∈ Ici a
Set.Annulus.iUnion_co_map_succ_eq_ci Special case a = ⊥ of biUnion_Ici_co_map_succ
Set.Annulus.iUnion_oc_map_succ_eq_oi Special case a = ⊥ of biUnion_Ici_oc_map_succ
Set.EAnnulus.oc Set.EAnnulus.oo has moved to Defs.lean
MeasureTheory.BoundedCompactSupport Bounded compactly supported measurable functions
MeasureTheory.BoundedCompactSupport.memLp Bounded compactly supported functions are in all Lᵖ spaces
MeasureTheory.BoundedCompactSupport.integrable Bounded compactly supported functions are integrable
MeasureTheory.BoundedCompactSupport.norm preferably use enorm
MeasureTheory.BoundedCompactSupport.integrable_mul doesn't use compact support but is convenient to have here
MeasureTheory.BoundedCompactSupport.starRingEnd This lemma is defeq to BoundedCompactSupport.conj, but starRingEnd and conj are both simp normal forms, so a lemma for each is needed
MeasureTheory.BoundedCompactSupport.mono If ‖f‖ is bounded by g and g is bounded compactly supported, then so is f
MeasureTheory.BoundedCompactSupport.mono_norm use mono preferably
MeasureTheory.BoundedCompactSupport.finset_sum A finite sum of bounded compactly supported functions is bounded compactly supported
MeasureTheory.BoundedCompactSupport.sq_eLpNorm_le_sums Used in Proposition 2.0.4
MeasureTheory.BoundedCompactSupport.prod_mul An elementary tensor of bounded compactly supported functions is bounded compactly supported
BoundedFiniteSupport.memLp Bounded finitely supported functions are in all Lᵖ spaces
BoundedFiniteSupport.integrable Bounded finitely supported functions are integrable
AllBallsCoverBalls.mk Prove AllBallsCoverBalls only for balls of positive radius
Metric.secondCountableTopology_of_almost_dense_set_balls_nat Documented declaration: secondCountableTopology_of_almost_dense_set_balls_nat
Metric.secondCountableTopology_of_almost_dense_set_balls A pseudometric space is second countable if, for every ε > 0 and every ball B, there is a countable set which is ε-dense in B
BallsCoverBalls.secondCountableTopology A pseudometric space is second countable if, for every ε > 0 and every ball B is covered by finitely many balls of radius ε
AllBallsCoverBalls.secondCountableTopology A pseudometric space is second countable if every ball of radius a * r is covered by b many balls of radius r
ENNReal.biSup_add_biSup unused
ENNReal.finsetSum_biSup unused
ENNReal.enorm_enorm_sub_enorm_le The reverse triangle inequality for enorm
Real.enorm_le_enorm Transfer an inequality over ℝ to one of ENorms over ℝ≥0∞
NNReal.div_self_eq_ite MR wonders: is this lemma actually used?
Real.nnnorm_le_nnnorm Transfer an inequality over ℝ to one of NNNorms over ℝ≥0
MeasureTheory.superlevelSet The superlevel set of a function f
MeasureTheory.distribution The distribution function of a function f
MeasureTheory.select_neighborhood_distribution TODO: better lemma name!
MeasureTheory.distribution_pow TODO: investigate generalising this to enorm classes This requires adding enorm versions of NormOneClass and NormMulClass
MeasureTheory.distribution_eq_zero_of_ae_zero_enorm TODO: make this an iff?
MeasureTheory.distribution_indicator_le_measure Lemma 1.1.24 of [Ian Tice]
MeasureTheory.distribution_indicator_add_of_support_subset_ennreal ENNReal version of the previous lemma
MeasureTheory.distribution_indicator_add_of_support_subset_nnreal NNReal version of the previous lemma
MeasureTheory.C_distribution_le_of_eLpNorm_le The constant used in C_distribution_le_of_eLpNorm_le
ENormedAddCommSubMonoid An enormed monoid is an additive monoid endowed with a continuous enorm
MeasureTheory.esub_zero unused
MeasureTheory._root_.ENNReal.toNNReal_smul TODO: find better place for this?
MeasureTheory.eLpNorm_const_nnreal_smul_le TODO: put next to MeasureTheory.eLpNorm_const_smul_le (which perhaps can stay)
MeasureTheory.eLpNorm_const_smul' TODO: put next to eLpNorm_const_smul
MeasureTheory.eLpNorm_const_smul'' TODO: put next to eLpNorm_const_smul
MeasureTheory.eLpNorm_const_smul''' TODO: put next to eLpNorm_const_smul
MeasureTheory.eLpNormEssSup_const_nnreal_smul_le TODO: put next to the unprimed version; perhaps both should stay
NNReal.smul_ennreal_eq_mul move to ENNReal.Basic or similar
hasWeakType_maximalFunction_one The proof is roughly between (9.0.12)-(9.0.22)
MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded move
MeasureTheory.LocallyIntegrable.integrableOn_ball move
continuous_average_ball unused in Carleson move to separate file (not sure where)
lowerSemiContinuousOn_integral_ball unused in Carleson move to separate file (not sure where)
MeasureTheory.HasLorentzType An operator has Lorentz type (p, r, q, s) if it is bounded as a map from L^{q, s} to L^{p, r}
MeasureTheory.HasRestrictedWeakType Defines when an operator "has restricted weak type"
MeasureTheory.HasRestrictedWeakType' An enhanced version of HasRestrictedWeakType
MeasureTheory.WeaklyContinuous The weak continuity assumption needed for HasRestrictedWeakType.hasLorentzType_helper
_root_.MeasureTheory.Integrable.conj move to Function/L1/Integrable.lean
_root_.MeasureTheory.Integrable.mul_conj TODO: compare with mul and conj in BoundedCompactSupport
MeasureTheory.eLorentzNorm_congr_enorm_ae Proof analogous to eLpNorm_congr_enorm_ae
MeasureTheory.eLorentzNorm_congr_ae Proof analogous to eLpNorm_congr_ae
MeasureTheory.eLorentzNorm'_eq Theorem 6.6 in https://doi.org/10.1007/978-3-319-30034-4
MeasureTheory.eLorentzNorm_eq TODO: remove this?
MeasureTheory.MemLorentz_of_MemLorentz_ge TODO: could maybe be strengthened to ↔
MeasureTheory.eLorentzNorm' The Lorentz seminorm of a function, for 0 < p < ∞
MeasureTheory.eLorentzNorm The Lorentz seminorm of a function
MeasureTheory.MemLorentz A function is in the Lorentz space L^{p,q} if it is (strongly a.e.)-measurable and has finite Lorentz seminorm
MeasureTheory.lorentz_helper The function k in the proof of Theorem 6.7 in https://doi.org/10.1007/978-3-319-30034-4
MeasureTheory.LorentzAddConst A constant for the inequality ‖f + g‖_{L^{p,q}} ≤ C * (‖f‖_{L^{p,q}} + ‖g‖_{L^{p,q}})
MeasureTheory.Lorentz TODO: basic results
MeasureTheory.eLpNormEssSup_map_measure' replace the unprimed mathlib version
MeasureTheory.eLpNorm_map_measure' replace the unprimed mathlib version
MeasureTheory.eLpNorm_comp_measurePreserving' replace the unprimed version
MeasureTheory.eLpNorm_iSup' Monotone convergence applied to eLpNorms
MeasureTheory.eLpNormEssSup_indicator_const_eq' complements the mathlib lemma eLpNormEssSup_indicator_const_eq
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x)
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm' Hölder's inequality, as an inequality on the ℒp seminorm for functions to ℝ≥0∞
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_enorm Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x)
MeasureTheory.SimpleFunc.measurable_comp TODO: tag this as @[fun_prop] (currently this gives an error)
MeasureTheory.SimpleFunc.induction₀ Proof stolen from the mathlib SimpleFunc.induction with a minor modification that is even suggested there
MeasureTheory.SimpleFunc.iSup_approx_apply' Version of iSup_approx_apply for ConditionallyCompleteLinearOrderBot
MeasureTheory.SimpleFunc.nnrealRatEmbed A sequence of ℝ≥0s such that its range is the set of non-negative rational numbers
MeasureTheory.SimpleFunc.nnapprox Approximate a function α → ℝ≥0 by a sequence of simple functions
MeasureTheory.Measurable.nnreal_induction modelled after Measurable.ennreal_induction but with very raw assumptions
MeasureTheory.Measurable.ennreal_induction' modified from ennreal_induction
MeasureTheory.Antitone.ennreal_induction' modified from ennreal_induction
enorm_algebraMap' move to Mathlib.Analysis.Normed.Module.Basic, next to nnnorm_algebraMap'
Function.Periodic.setIntegral_Ioc_add_eq If f is a periodic function with period T, then its integral over [t, t + T] does not depend on t
Function.Periodic.eLpNorm TODO: the assumption p ≠ ⊤ is not necessary; this case should be proved as well
MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc Analogous to MeasureTheory.MemLp.memLp_liftIoc
MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc' TODO: find better name
MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul The layer cake formula / Cavalieri's principle / tail probability formula: Let f be a non-negative measurable function on a measure space
MeasureTheory.lintegral_eq_lintegral_distribution Documented declaration: lintegral_eq_lintegral_distribution
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul' The layer cake formula / Cavalieri's principle / tail probability formula: Let f be a non-negative measurable function on a measure space
MeasureTheory.lintegral_eq_lintegral_meas_le' Documented declaration: lintegral_eq_lintegral_meas_le'
ENNReal.Lp_add_le_sum Minkowski inequality for finite sums of ENNReal-valued functions
ENNReal.lintegral_prod_norm_pow_le' A version of Hölder with multiple arguments, allowing ∞ as an exponent
ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm Hölder's inequality for functions α → ℝ≥0∞, using exponents in ℝ≥0∞
ENNReal.sq_lintegral_mul_le_mul_lintegral_sq Cauchy–Schwarz inequality for functions α → ℝ≥0∞ (Hölder's inequality squared)
r_sub_p_nonneg Used in the proof of Young's convolution inequality
ENNReal.convolution_zero_of_c_nonpos Used to handle trivial case c ≤ 0 when proving versions of Young's convolution inequality assuming ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)
ENNReal.eLpNorm_top_convolution_le_aux Auxiliary inequality used to prove inequalities with simpler conditions on f and g
ENNReal.eLpNorm_top_convolution_le Special case of Young's convolution inequality when r = ∞
ENNReal.eLpNorm_top_convolution_le' Special case of Young's convolution inequality when r = ∞
ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm This inequality is used in the proof of Young's convolution inequality eLpNorm_convolution_le_ofReal
ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm' This inequality is used in the proof of Young's convolution inequality eLpNorm_convolution_le_ofReal'
ENNReal.eLpNorm_convolution_le_ofReal_aux Auxiliary inequality used to prove versions with simpler conditions on f and g
ENNReal.eLpNorm_convolution_le_of_norm_le_mul_aux Auxiliary result to prove the following versions with simpler assumptions on f and g
ENNReal.eLpNorm_convolution_le_of_norm_le_mul Documented declaration: eLpNorm_convolution_le_of_norm_le_mul
ENNReal.eLpNorm_convolution_le_of_norm_le_mul' Documented declaration: eLpNorm_convolution_le_of_norm_le_mul'
ENNReal.eLpNorm_convolution_le_enorm_mul Documented declaration: eLpNorm_convolution_le_enorm_mul
ENNReal.eLpNorm_convolution_le_enorm_mul' Documented declaration: eLpNorm_convolution_le_enorm_mul'
ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul Documented declaration: eLpNorm_Ioc_convolution_le_of_norm_le_mul
ENNReal.eLpNorm_Ioc_convolution_le_enorm_mul Documented declaration: eLpNorm_Ioc_convolution_le_enorm_mul
lintegral_antitone_mul_le This is Theorem 4.19 in https://doi.org/10.1007/978-3-319-30034-4
AddCircle.measurable_equivIoc Add before measurableEquivIoc
AddCircle.measurableEquivIoc' Replacement for existing proof of measurableEquivIoc now that the proof of measurable_toFun is extracted as a separate lemma
AddCircle.measurableEquivIco' Replacement for existing proof of measurableEquivIco now that the proof of measurable_toFun is extracted as a separate lemma
AddCircle.eLpNorm_liftIoc The norm of the lift of a function f is equal to the norm of f on that period
AddCircle.eLpNorm_liftIoc' The norm of the lift of a function f is equal to the norm of f on that period
AddCircle.eLpNorm_liftIco The norm of the lift of a function f is equal to the norm of f on that period
AddCircle.eLpNorm_liftIco' The norm of the lift of a function f is equal to the norm of f on that period
AddCircle.eLpNorm_liftIoc_of_periodic The norm of the lift of a periodic function f is equal to the norm of f on any period
AddCircle.eLpNorm_liftIoc_of_periodic' The norm of the lift of a periodic function f is equal to the norm of f on any period
AddCircle.eLpNorm_liftIco_of_periodic The norm of the lift of a periodic function f is equal to the norm of f on any period
AddCircle.eLpNorm_liftIco_of_periodic' The norm of the lift of a periodic function f is equal to the norm of f on any period
MeasureTheory.aeMeasurable_withDensity_inv TODO: generalize this to other measures and density functions?
As The blow-up factor of repeatedly increasing the size of balls
MeasureTheory.Nat.exists_max_image todo: move
MeasureTheory.measureReal_ball_le_same' Version of measureReal_ball_le_same without ceiling function
ENNReal.ofNNReal_preimage TODO: move these lemmas somewhere else?
ENNReal.map_toReal_eq_map_toReal_comap_ofReal TODO: move these lemmas somewhere else?
Measure.Subtype.noAtoms TODO: move this general result to an appropriate place TODO: maybe generalize further to general measures restricted to a subtype
Measure.Subtype.sigmaFinite TODO: move this general result to an appropriate place TODO: maybe generalize further to general measures restricted to a subtype
measurableEmbedding_ofNNReal TODO: move?
NNReal.toReal_Iio_eq_Ico TODO: move somewhere else and add more lemmas for Ioo, Ico etc
ENNReal.toReal_Iio_eq_Ico TODO: move somewhere else and add more lemmas for Ioo, Ico etc
ENNReal.toReal_Icc_eq_Icc TODO: move somewhere else and add more lemmas for Ioo, Ico etc
ENNReal.toReal_Ioo_eq_Ioo TODO: move somewhere else and add more lemmas for Ioo, Ico etc
ENNReal.toReal_Ioo_top_eq_Ioi TODO: move somewhere else and add more lemmas for Ioo, Ico etc
ENNReal.toReal_Ioi_eq_Ioi TODO: move somewhere else and add more lemmas for Ioo, Ico etc
ENNReal.Ioi_eq_Ioc_top TODO: move somewhere else?
lintegral_nnreal_eq_lintegral_toNNReal_Ioi TODO: are there better names?
lintegral_nnreal_toReal_eq_lintegral_Ioi TODO: do we actually use this?
MeasureTheory.NoAtoms'.measure_comap_eq_subtype_coe TODO: move
MeasureTheory.NoAtoms'.PFun.ofGraph' Constructs a partial function `α →
MeasureTheory.NoAtoms'.PFun.insert Gives the partial function sending a to b and agreeing with f otherwise
MeasureTheory.NoAtoms'.PFun.Monotone The property of a partial function f to be monotone, i.e. f a ≤ f b whenever a ≤ b and both a and b are in the domain of f
MeasureTheory.NoAtoms'.TopologicalSpace.SeparableSpace.subtype TODO: move
MeasureTheory.NoAtoms'.ClosedIicTopology.subtype TODO: move
MeasureTheory.NoAtoms'.instIsCountablyGenerated_atTop TODO: move
MeasureTheory.NoAtoms'.instIsCountablyGenerated_atBot TODO: move
MeasureTheory.IsAtom An atom of a measure μ is a set s of positive measure for which all measurable subsets either have measure 0 or μ s
MeasureTheory.NoAtoms' Measure μ has no atoms if for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s
MeasureTheory.NoAtoms'.instNullSingletonClass' TODO: Do we really need SigmaFinite μ or is SFinite μ sufficient?
MeasureTheory.essProjFst For a (s : Set (α × β)) and (ν : Measure β), we define essProjFst such that x ∈ essProjFst s ν iff 0 < ν {y | ⟨x, y⟩ ∈ s}
MeasureTheory.essProjSnd For a (s : Set (α × β)) and (μ : Measure α), we define essProjSnd such that y ∈ essProjSnd s μ iff 0 < μ {x | ⟨x, y⟩ ∈ s}
MeasureTheory.setLIntegral_strict_mono_set TODO: move
MeasureTheory.isAtom_swap_iff TODO: move?
MeasureTheory.AEMeasurable.lintegral_prod_right' Proof copied from MeasureTheory.AEStronglyMeasurable.integral_prod_right' Was it intentional that there's no left version?
MeasureTheory.AEMeasurable.lintegral_prod_right XXX: the corresponding result for AEStronglyMeasurable doesn't exist; should it be added?
Set.minLayer The nth minimal layer of A
Set.maxLayer The nth maximal layer of A
Set.layersAbove The elements above A's n minimal layers
Set.layersBelow The elements below A's n maximal layers
Set.minLayer_zero XXX(MR): should this and maxLayer_zero be simp?
Set.subtype_mk_minimal_iff XXX: is this in mathlib already/can it also be removed?
Set.minLayer_eq_setOf_height A.minLayer n comprises exactly A's elements of height n
Set.iUnion_minLayer_iff_bounded_series A equals the union of its minLayers up to n iff all LTSeries in A have length at most n
Real.le_pow_natCeil_logb to Mathlib.Analysis.SpecialFunctions.Log.Base
iSup_rpow TODO: this helper lemma may be useful in other places to, for instance in HardyLittlewood.lean
MeasureTheory.laverage_add_left Named for consistency with lintegral_add_left' Maybe add laverage/laverage theorems for all the other lintegral_add statements?
MeasureTheory.laverage_mono Named for consistency with lintegral_mono'
MeasureTheory.setLaverage_add_left' Named for consistency with lintegral_add_left' Maybe add laverage/setLaverage theorems for all the other lintegral_add statements?
MeasureTheory.setLaverage_mono' Named for consistency with setLintegral_mono'
MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj One of the very few cases where a norm can be moved out of an integral
EquivalenceOn An equivalence relation on the set s
EquivalenceOn.setoid The setoid defined from an equivalence relation on a set
EquivalenceOn.out An arbitrary representative of x w.r.t
EquivalenceOn.reprs The set of representatives of an equivalence relation on a set
norm_indicator_one_le for mathlib?
MeasureTheory.Integrable.indicator_const must be in mathlib but can't find it
ENNReal.ofReal_zpow Analogous to ENNReal.ofReal_pow in Mathlib Currently unused
prod_attach_insert TODO: to mathlib
iSup_eq_iSup currently unused
ciSup_eq_ciSup currently unused
ENNReal.mem_sub_Ioo the Ioc version is true for r = ∞ also
ENNReal.coe_rpow_ne_top' Note this lemma can directly be applied to elements of ℝ≥0 as well
ENNReal.exp_toReal_pos' unused (one reference in an also-unused lemma)
ENNReal.toReal_mem_Ioo XXX: generalise interval bounds!
ENNReal.ofReal_mem_Ioo_0_1 XXX: generalise interval bounds!
ENNReal.eq_of_rpow_eq TODO: check which ones are actually used
ENNReal.preservation_positivity₀ TODO: find a better name for the next three lemmas!
ENNReal.rpow_apply_coe TODO: should some of the following lemmas be tagged with finiteness?
ENNReal.power_estimate TODO: better name!
ENNReal.power_estimate' TODO: better name!
ENNReal.rpow_le_rpow_of_exponent_le_base_le_enorm Note: this lemma is false if t = γ = ∞ and a < 0 ≤ b, as then t ^ a = ∞ ^ a = 0 and the statement becomes ∞ ≤ 0 * ∞ = 0
ENNReal.rpow_le_rpow_of_exponent_le_base_ge TODO: there is a lot of overlap between above proof and below
ComputationsInterpolatedExponents.exp_toReal_ne_zero_of_Ico unused
ComputationsInterpolatedExponents.interpolated_pos' TODO: remove, this is redundant, but for now mirror the development for reals
ComputationsChoiceExponent.eq_exponents₃ TODO: simplify these proofs with statements above
C_LorentzInterpolation The constant occurring in the general real interpolation theorem (for Lorentz spaces)
exists_hasLorentzType_real_interpolation General Marcinkiewicz real interpolation theorem
MeasureTheory.SubadditiveOn The operator is subadditive on functions satisfying P with constant A
MeasureTheory.AESubadditiveOn The operator is subadditive on functions satisfying P with constant A (this is almost vacuous if A = ⊤)
MeasureTheory.SubadditiveOn.const If T is constant in the second argument (but not necessarily the first) and satisfies a subadditivity criterion, then SubadditiveOn T P 1
MeasureTheory.AESubadditiveOn.const If T is constant in the second argument (but not necessarily the first) and satisfies a subadditivity criterion, then AESubadditiveOn T P 1
MeasureTheory.SublinearOn The operator is sublinear on functions satisfying P with constant A
MeasureTheory.AESublinearOn The operator is almost everywhere sublinear on functions satisfying P with constant A
MeasureTheory.SublinearOn.const If T is constant in the second argument (but not necessarily the first) and satisfies certain requirements, then SublinearOn T P 1
MeasureTheory.AESublinearOn.const If T is constant in the second argument (but not necessarily the first) and satisfies certain requirements, then AESublinearOn T P 1
MeasureTheory.PreservesAEStrongMeasurability Proposition that expresses that the map T map between function spaces preserves AE strong measurability on L^p
MeasureTheory.ton_measurable_eLpNorm_trunc TODO: the infrastructure can perhaps be improved here
MeasureTheory.exists_hasStrongType_real_interpolation_aux₀ The trivial case for the estimate in the real interpolation theorem when the L^p norm of f vanishes
MeasureTheory.exists_hasStrongType_real_interpolation_aux The estimate for the real interpolation theorem in case p₀ < p₁
MeasureTheory.exists_hasStrongType_real_interpolation_aux₁ TODO: the below lemmas were split because otherwise the lean server would crash (seems to be related to the linter?) (after the merge)
MeasureTheory.exists_hasStrongType_real_interpolation_aux₂ The main estimate in the real interpolation theorem for p₀ = p₁, before taking roots, for the case q₀ < q₁
MeasureTheory.exists_hasStrongType_real_interpolation_aux₃ The main estimate for the real interpolation theorem for p₀ = p₁, requiring q₀ ≠ q₁, before taking roots
MeasureTheory.exists_hasStrongType_real_interpolation_aux₄ The main estimate for the real interpolation theorem, before taking roots, combining the cases p₀ ≠ p₁ and p₀ = p₁
MeasureTheory.C_realInterpolation_ENNReal The definition of the constant in the real interpolation theorem, when viewed as an element of ℝ≥0∞
MeasureTheory.C_realInterpolation The constant occurring in the real interpolation theorem
MeasureTheory.exists_hasStrongType_real_interpolation Marcinkiewicz real interpolation theorem
MeasureTheory.representationLp Characterization of ∫⁻ x : α, f x ^ p ∂μ by a duality argument
MeasureTheory.aemeasurability_prod₁ TODO: better name!
MeasureTheory.aemeasurability_prod₂ TODO: better name!
MeasureTheory.aemeasurable_integral_component TODO: better name!
MeasureTheory.lintegral_lintegral_pow_swap Minkowsi's integral inequality: TODO describe what it does
MeasureTheory.indicator_ton_measurable TODO: better name!
MeasureTheory.indicator_ton_measurable_lt TODO: better name!
MeasureTheory.restrict_to_support TODO: better name!
MeasureTheory.restrict_to_support_truncCompl TODO: better name!
MeasureTheory.restrict_to_support_trnc TODO: better name!
MeasureTheory.estimate_trnc One of the key estimates for the real interpolation theorem, not yet using the particular choice of exponent and scale in the ScaledPowerFunction
MeasureTheory.sel TODO: add a doc-string, explaining the purpose of this definition
MeasureTheory.estimate_trnc₁ Documented declaration: estimate_trnc₁
MeasureTheory.weaktype_aux₀ If T has weaktype p₀-p₁, f is AEStronglyMeasurable and the p-norm of f vanishes, then the q-norm of T f vanishes
MeasureTheory.weaktype_estimate_trunc TODO: can we remove the hypothesis on a?
MeasureTheory.weaktype_estimate_trunc_top NB
ScaledPowerFunction A ScaledPowerFunction is meant to represent a function of the form t ↦ (t / d)^σ, where d is strictly positive and either σ > 0 or σ < 0
ToneCouple A ToneCouple is a couple of two monotone functions that are practically inverses of each other
StrictRangeToneCouple A StrictRangeToneCouple is a ToneCouple for which the functions in the couple, when restricted to Ioo 0 ∞, map to Ioo 0 ∞
spf_to_tc A scaled power function gives rise to a ToneCouple
ChoiceScale.d_pos If the p-norm of f is positive and finite, then d is positive
ChoiceScale.spf_ch The particular choice of scaled power function that works in the proof of the real interpolation theorem
MeasureTheory.lintegral_double_restrict_set TODO: change lhs and rhs?
MeasureTheory.lintegral_rw_aux local convenience function
MeasureTheory.trunc The t-truncation of a function f
MeasureTheory.truncCompl The complement of a t-truncation of a function f
MeasureTheory.trnc A function to deal with truncations and complement of truncations in one go
MeasureTheory.trunc_add_truncCompl A function is the complement if its truncation and the complement of the truncation
MeasureTheory.coe_coe_eq_ofReal A small lemma that is helpful for rewriting
MeasureTheory.eLpNorm_trunc_mono The norm of the truncation is monotone in the truncation parameter
MeasureTheory.eLpNorm_truncCompl_anti The norm of the complement of the truncation is antitone in the truncation parameter
MeasureTheory.eLpNorm_trunc_measurable The norm of the truncation is meaurable in the truncation parameter
MeasureTheory.eLpNorm_truncCompl_measurable The norm of the complement of the truncation is measurable in the truncation parameter
MeasureTheory.estimate_eLpNorm_truncCompl TODO: better name!
MeasureTheory.estimate_eLpNorm_trunc TODO: better name!
MeasureTheory.trunc_Lp_Lq_higher If f is in Lp, the truncation is element of Lq for q ≥ p
MeasureTheory.truncCompl_Lp_Lq_lower If f is in Lp, the complement of the truncation is in Lq for q ≤ p
MeasureTheory.memLp_of_memLp_le_of_memLp_ge Lemma 6.10 in Folland XXX: is the ContinuousAdd hypothesis really necessary for MemLp.add (and hence here)?
MeasureTheory.res'comp₀ TODO: this one is probably obsolete
MeasureTheory.lintegral_Ioi_rpow_of_lt_abs TODO: treat symmetrically to Ioo case?
MeasureTheory.AEStronglyMeasurable.induction TODO: move to a lower-level file!
MeasureTheory.rearrangement The decreasing rearrangement function f^#
MeasureTheory.lt_rearrangement_iff_lt_distribution Lemma 1.1.22 of [Ian Tice]
MeasureTheory.continuousWithinAt_rearrangement Lemma 1.1.22 of [Ian Tice]
MeasureTheory.rearrangement_indicator_le Lemma 1.1.24 of [Ian Tice]
MeasureTheory.lintegral_rearrangement_pow Lemma 1.1.22 of [Ian Tice]
MeasureTheory.sSup_rearrangement Lemma 1.1.22 of [Ian Tice]
MeasureTheory.rearrangement_zero_eq_eLpNormEssSup Lemma 1.1.22 of [Ian Tice]
MeasureTheory.setLIntegral_enorm_le_lintegral_rearrangement Lemma 1.1.24 of [Ian Tice]
MeasureTheory.lintegral_rearrangement_eq Theorem 4.17 in https://doi.org/10.1007/978-3-319-30034-4
MeasureTheory.lintegral_rearrangement_add_rearrangement_le_add_lintegral Remark 4.18 in https://doi.org/10.1007/978-3-319-30034-4
ContinuousWithinAt.measure_lt_ne_zero TODO: generalize?
eLpNormEssSup_eq_iSup' TODO: generalize?
eLpNormEssSup_nnreal_eq_iSup_nnreal TODO: generalize?
AddCircle.liftIco_eq_liftIco If f has period p, then every lift of f to AddCircle p is the same
AddCircle.liftIoc_eq_liftIoc If f has period p, then every lift of f to AddCircle p is the same
AddCircle.liftIco_eq_liftIoc If f has period p, then every lift of f to AddCircle p is the same
MeasureTheory.wnorm' The weak L^p norm of a function, for p < ∞
MeasureTheory.wnorm The weak L^p norm of a function
MeasureTheory.MemWLp A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm
MeasureTheory.MemWLp.ae_ne_top If a function f is MemWLp, then its norm is almost everywhere finite
MeasureTheory.HasWeakType An operator has weak type (p, q) if it is bounded as a map from L^p to weak L^q
MeasureTheory.HasBoundedWeakType A weaker version of HasWeakType
MeasureTheory.HasStrongType An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q
MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff move
MeasureTheory.distribution_smul_left Documented declaration: distribution_smul_left
MeasureTheory.HasWeakType.const_smul' TODO: do we want to unify this lemma with its unprimed version, perhaps using an ENormedSemiring class?
MeasureTheory.HasWeakType.const_mul' TODO: do we want to unify this lemma with its unprimed version, perhaps using an ENormedSemiring class?
MeasureTheory.lintegral_norm_pow_eq_distribution The layer-cake theorem, or Cavalieri's principle for functions into a space with a continuous enorm
MeasureTheory.eLpNorm_pow_eq_distribution The layer-cake theorem, or Cavalieri's principle, written using eLpNorm
MeasureTheory.eLpNorm_eq_distribution The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without taking powers
czOperator The Calderon Zygmund operator T_r in chapter Two-sided Metric Space Carleson
czOperator_aestronglyMeasurable_aux Next lemma is useful for fun_prop in a context where it can not find the relevant measure to apply czOperator_aestronglyMeasurable
czOperator_sub This could be adapted to state T_r is a linear operator but maybe it's not worth the effort
geometric_series_estimate Lemma 10.1.1
C10_0_1 The constant used in two_sided_metric_carleson
two_sided_metric_carleson Theorem 10.0.1
simpleNontangentialOperator The operator T_*^r g(x), defined in (10.1.31), above Lemma 10.1.6
estimate_x_shift Lemma 10.1.2
cotlar_control Lemma 10.1.3
cotlar_set_F₁ Part 1 of Lemma 10.1.4 about F₁
cotlar_set_F₂ Part 2 of Lemma 10.1.4 about F₂
cotlar_estimate Lemma 10.1.5
lowerSemicontinuous_simpleNontangentialOperator Part of Lemma 10.1.6
simple_nontangential_operator Lemma 10.1.6
simple_nontangential_operator_le This is the first step of the proof of Lemma 10.0.2, and should follow from 10.1.6 + monotone convergence theorem
small_annulus_right Part of Lemma 10.1.7, reformulated
small_annulus_left Part of Lemma 10.1.7, reformulated
nontangential_operator_boundary Lemma 10.1.8
lowerSemicontinuous_nontangentialOperator Part of Lemma 10.1.6
nontangential_from_simple Lemma 10.0.2
two_sided_metric_carleson_hasRestrictedWeakType Theorem 10.0.1, reformulation
two_sided_metric_carleson_hasLorentzType
interpolation_param The parameter where linear interpolation between t₀ and t₁ results in t
interpolation_param_interpolation TODO: move
interpolation_param_mem_Ioo TODO: move
C_carleson_hasStrongType The constant used in two_sided_metric_carleson_hasStrongType
C_carleson_hasStrongType_pos The constant used in two_sided_metric_carleson_hasStrongType
two_sided_metric_carleson_hasStrongType Strong-type bound for the Carleson operator (Theorem 10.0.1) after C_carleson_hasStrongType, two_sided_metric_carleson_hasLorentzType
IsTwoSidedKernel K is a two-sided Calderon-Zygmund kernel
maximal_theorem Lemma 10.2.1, formulated differently
maximal_theorem'' Alternate version of maximal_theorem'
lebesgue_differentiation Lemma 10.2.2
depth δ(x) in the blueprint
depth_pos_iff_mem A point's depth in an open set O is positive iff it lies in O
depth_lt_top_iff_ne_univ A point has finite depth in O iff O is not the whole space
depth_le_edist_add_depth A "triangle inequality" for depths
ball_covering' Lemma 10.2.4, but following the blueprint exactly (with a countable set of centres rather than functions from ℕ)
ball_covering Lemma 10.2.4
GeneralCase The property specifying whether we are in the "general case"
volume_lt_of_not_GeneralCase In the finite case, the volume of X is finite
czCenter The center of B_j in the proof of Lemma 10.2.5 (general case)
czRadius The radius of B_j in the proof of Lemma 10.2.5 (general case)
czBall The ball B_j in the proof of Lemma 10.2.5 (general case)
czBall6 The ball B_j' introduced below Lemma 10.2.5 (general case)
czBall3 The ball B_j* in Lemma 10.2.5 (general case)
czBall7 The ball B_j in the proof of Lemma 10.2.5 (general case)
encard_czBall3_le Part of Lemma 10.2.5 (general case)
czPartition Q_i in the proof of Lemma 10.2.5 (general case)
laverage_czBall7_le Inequality (10.2.30)
czApproximation The function g in Lemma 10.2.5
czRemainder' The function b_i in Lemma 10.2.5 (general case)
czRemainder The function b = ∑ⱼ bⱼ introduced below Lemma 10.2.5
tsum_czRemainder' Part of Lemma 10.2.5, this is essentially (10.2.16) (both cases)
aemeasurable_czApproximation Part of Lemma 10.2.5 (both cases)
BoundedFiniteSupport.czApproximation Part of Lemma 10.2.5 (both cases)
czApproximation_add_czRemainder Part of Lemma 10.2.5, equation (10.2.16) (both cases)
enorm_czApproximation_le_finite Equation (10.2.17), finite case
enorm_czApproximation_le_infinite Equation (10.2.17) specialized to the general case
enorm_czApproximation_le Part of Lemma 10.2.5, equation (10.2.17) (both cases)
eLpNorm_czApproximation_le_finite Equation (10.2.18), finite case
eLpNorm_czApproximation_le_infinite Equation (10.2.18), infinite case
eLpNorm_czApproximation_le Part of Lemma 10.2.5, equation (10.2.18) (both cases)
support_czRemainder'_subset Part of Lemma 10.2.5, equation (10.2.19) (general case)
integral_czRemainder' Part of Lemma 10.2.5, equation (10.2.20) (general case)
integral_czRemainder Part of Lemma 10.2.5, equation (10.2.20) (finite case)
ineq_10_2_32 Inequality (10.2.32)
eLpNorm_czRemainder'_le Part of Lemma 10.2.5, equation (10.2.21) (general case)
eLpNorm_restrict_czRemainder'_le Weaker version of eLpNorm_czRemainder'_le which is used repeatedly below
eLpNorm_czRemainder_le' Used to prove eLpNorm_czRemainder_le and tsum_eLpNorm_czRemainder_le
eLpNorm_czRemainder_le Part of Lemma 10.2.5, equation (10.2.21) (finite case)
tsum_volume_czBall3_le Part of Lemma 10.2.5, equation (10.2.22) (general case)
volume_univ_le Part of Lemma 10.2.5, equation (10.2.22) (finite case)
tsum_eLpNorm_czRemainder'_le Part of Lemma 10.2.5, equation (10.2.23) (general case)
tsum_eLpNorm_czRemainder_le Part of Lemma 10.2.5, equation (10.2.23) (finite case)
Ω The set Ω introduced below Lemma 10.2.5
α' Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound
α'_pos Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound
estimate_good Lemma 10.2.6
czOperatorBound The function F defined in Lemma 10.2.7
lemma_10_2_7_bound' Auxiliary bound used to prove lemma_10_2_7_bound
lemma_10_2_7_bound Bound used twice in the proof of Lemma 10.2.7
𝒥₂_bound The bounds on ‖czOperator K r (czRemainder' hX j) x‖ₑ used for the 𝒥₂ estimate (even though this part of the estimate doesn't require j ∈ 𝒥₂)
A_subset (10.2.52)
tsum_integral_K_le Long calculation toward the end of Lemma 10.2.7
estimate_bad_partial Lemma 10.2.7
distribution_czOperatorBound Lemma 10.2.8
estimate_bad Lemma 10.2.9
estimate_czOperator Lemma 10.0.3, blueprint form
czOperator_weak_1_1 Lemma 10.0.3, formulated differently
classical_carleson'@Challenge.lean Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions