Trust

Axioms come from the Lean kernel (Lean (version 4.34.0-rc2, x86_64-w64-windows-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.

Lake environment and dependency-pin digest: a3de9b3963c20711.

Verification scope: all declaration-bearing files; 118 of 118 eligible files selected, 3030 declarations requested.

Rendering mode: clean content-bound cache results only; 0 selected files had no reusable result and remain UNKNOWN. No Lean process was started for those misses during this static-site build.

Per-file probe bounds: 300 seconds. A resource stop is UNKNOWN, never a failed proof.

no axioms

10

standard axioms

2754

sorry

27

extra axioms

0

unknown

239

What the badges mean

no axioms

Lean's kernel checked the proof, and it rests on nothing but Lean's rules.

standard axioms

Checked by the kernel, using only propext, Classical.choice or Quot.sound: the three axioms nearly all of mathematics in Lean uses.

extra axioms

Checked by the kernel, but it assumes something the project declared with `axiom`. It is only as true as those assumptions.

depends on sorry

Not proved: somewhere in it, or in something it uses, a proof was left out (`sorry`).

trust unknown

Lean did not check it: Lean was not run, the file did not elaborate, or Lean has no constant by that name.

Trust UNKNOWN declarations (239)

1. ineq_aux_2_0_3 Carleson/Antichain/AntichainOperator.lean trust unknown: Lean has no constant by this name
2. Antichain.𝔄_aux_sum_splits Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
3. Antichain.𝔄_min_sum_le Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
4. Antichain.exists_p'_ge_L Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
5. Antichain.SL_nonempty Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
6. Antichain.p' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
7. Antichain.p'_mem Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
8. Antichain.L_le_I_p' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
9. Antichain.not_I_p'_le_L Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
10. Antichain.s_L_le_s_p' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
11. Antichain.L'_not_mem Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
12. Antichain.L'_le_I_p' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
13. Antichain.exists_p''_le_L' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
14. Antichain.exists_pΘ_eq_L' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
15. Antichain.eq_6_3_35 Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
16. Antichain.eq_6_3_37 Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
17. Antichain.ineq_6_3_36 Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
18. Antichain.ineq_6_3_38 Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
19. Antichain.ineq_6_3_39 Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
20. Antichain.volume_L'_le Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
21. Antichain.volume_union_I_p_eq_sum Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
22. Antichain.lhs' Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
23. Antichain.lhs Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
24. Antichain.le_C6_3_4 Carleson/Antichain/AntichainTileCount.lean trust unknown: Lean has no constant by this name
25. ineq_6_1_7 Carleson/Antichain/Basic.lean trust unknown: Lean has no constant by this name
26. Tile.aux_6_2_3 Carleson/Antichain/TileCorrelation.lean trust unknown: Lean has no constant by this name
27. Tile.e625 Carleson/Antichain/TileCorrelation.lean trust unknown: Lean has no constant by this name
28. Tile.ineq_6_2_16 Carleson/Antichain/TileCorrelation.lean trust unknown: Lean has no constant by this name
29. Tile.exp_ineq Carleson/Antichain/TileCorrelation.lean trust unknown: Lean has no constant by this name
30. Qᵣ Carleson/Classical/CarlesonOperatorReal.lean trust unknown: Lean has no constant by this name
31. Qᵣ_dense Carleson/Classical/CarlesonOperatorReal.lean trust unknown: Lean has no constant by this name
32. Qᵣ_countable Carleson/Classical/CarlesonOperatorReal.lean trust unknown: Lean has no constant by this name
33. norm_modulationOperator Carleson/Classical/HilbertStrongType.lean trust unknown: Lean has no constant by this name
34. indicator_modulationOperator Carleson/Classical/HilbertStrongType.lean trust unknown: Lean has no constant by this name
35. eLpNorm_modulationOperator Carleson/Classical/HilbertStrongType.lean trust unknown: Lean has no constant by this name
36. eLpNorm_indicator_modulationOperator Carleson/Classical/HilbertStrongType.lean trust unknown: Lean has no constant by this name
37. big_ball Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
38. x_mem_𝓘u Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
39. 𝒬m_mem_ball Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
40. 𝓘_not_lt_𝓘 Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
41. 𝓘_eq_𝓘 Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
42. ball_eq_ball Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
43. disjoint_balls Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
44. mem_big_ball Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
45. subset_big_ball Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
46. balls_cover_big_ball Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
47. 𝒬_injOn_𝔘m Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
48. card_𝔘m_le Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
49. 𝔐' Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
50. interchange Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
51. indicator_le Carleson/Discrete/ExceptionalSet.lean trust unknown: Lean has no constant by this name
52. two_mul_n_add_six_lt Carleson/Discrete/ForestComplement.lean trust unknown: Lean has no constant by this name
53. ℭ₁' Carleson/Discrete/ForestComplement.lean trust unknown: Lean has no constant by this name
54. carlesonOperatorIntegrand_const_smul Carleson/DoublingMeasure.lean trust unknown: Lean has no constant by this name
55. linearizedCarlesonOperator_const_smul Carleson/DoublingMeasure.lean trust unknown: Lean has no constant by this name
56. carlesonOperatorIntegrand_const_smul' Carleson/DoublingMeasure.lean trust unknown: Lean has no constant by this name
57. linearizedCarlesonOperator_const_smul' Carleson/DoublingMeasure.lean trust unknown: Lean has no constant by this name
58. 𝔓X_s Carleson/FinitaryCarleson.lean trust unknown: Lean has no constant by this name
59. 𝔰_eq Carleson/FinitaryCarleson.lean trust unknown: Lean has no constant by this name
60. 𝔓_biUnion Carleson/FinitaryCarleson.lean trust unknown: Lean has no constant by this name
61. sum_eq_zero_of_notMem_Icc Carleson/FinitaryCarleson.lean trust unknown: Lean has no constant by this name
62. K' Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
63. K'.eq_K Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
64. K'.integrableOn_mul_f Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
65. K'.support_subset Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
66. K'.enorm_le_enorm_K Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
67. annulus_integral_bound Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
68. TileStructure.Forest.nontangential_integral_bound₁ Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
69. TileStructure.Forest.nontangential_integral_bound₂ Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
70. TileStructure.Forest.nontangential_pointwise_bound Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
71. TileStructure.Forest.eI𝒬u_mul Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
72. TileStructure.Forest.boundedCompactSupport_eI𝒬u_mul Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
73. TileStructure.Forest.norm_eI𝒬u_mul_eq Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
74. TileStructure.Forest.cS_bound Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
75. TileStructure.Forest.aeMeasurable_cS_bound Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
76. TileStructure.Forest.le_C7_2_1 Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
77. TileStructure.Forest.eLpNorm_two_cS_bound_le Carleson/ForestOperator/L2Estimate.lean trust unknown: Lean has no constant by this name
78. TileStructure.Forest.exists_p_of_mem_σ Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
79. TileStructure.Forest.σMax_mem_σ Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
80. TileStructure.Forest.s_le_s_of_mem_𝓛 Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
81. TileStructure.Forest.subset_of_mem_𝓛 Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
82. TileStructure.Forest.mem_𝓙_of_mem_𝓙' Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
83. TileStructure.Forest.exp_Lipschitz Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
84. TileStructure.Forest.exp_sub_one_le Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
85. TileStructure.Forest.dist_lt_5 Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
86. TileStructure.Forest.L7_1_4_bound Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
87. TileStructure.Forest.L7_1_4_integrand_bound Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
88. TileStructure.Forest.sum_pow_two_le Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
89. TileStructure.Forest.L7_1_4_sum Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
90. TileStructure.Forest.L7_1_4_dist_le Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
91. TileStructure.Forest.s_le_s Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
92. TileStructure.Forest.ball_covered_by_𝓙 Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
93. TileStructure.Forest.Grid_subset_ball' Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
94. TileStructure.Forest.L7_1_4_integral_le_integral Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
95. TileStructure.Forest.L7_1_4_laverage_le_MB Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
96. TileStructure.Forest.p_sum_eq_s_sum Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
97. TileStructure.Forest.L7_1_6_integral_eq Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
98. TileStructure.Forest.L7_1_6_integral_le Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
99. TileStructure.Forest.L7_1_6_I_le Carleson/ForestOperator/PointwiseEstimate.lean trust unknown: Lean has no constant by this name
100. TileStructure.Forest.le_C7_3_3_exponent Carleson/ForestOperator/QuantativeEstimate.lean trust unknown: Lean has no constant by this name
101. TileStructure.Forest.local_dens2_tree_bound_aux Carleson/ForestOperator/QuantativeEstimate.lean trust unknown: Lean has no constant by this name
102. TileStructure.Forest.local_dens2_tree_bound_aux' Carleson/ForestOperator/QuantativeEstimate.lean trust unknown: Lean has no constant by this name
103. TileStructure.Forest.eLpNorm_approxOnCube_two_le Carleson/ForestOperator/QuantativeEstimate.lean trust unknown: Lean has no constant by this name
104. TileStructure.Forest.density_tree_bound_aux Carleson/ForestOperator/QuantativeEstimate.lean trust unknown: Lean has no constant by this name
105. _root_.MeasureTheory.BoundedCompactSupport.const_smul Carleson/ForestOperator/QuantativeEstimate.lean trust unknown: Lean has no constant by this name
106. Grid._root_.C2_1_2 Carleson/GridStructure.lean trust unknown: Lean has no constant by this name
107. Grid._root_.C2_1_2_le_inv_256 Carleson/GridStructure.lean trust unknown: Lean has no constant by this name
108. Grid._root_.C2_1_2_le_one Carleson/GridStructure.lean trust unknown: Lean has no constant by this name
109. Grid._root_.C2_1_2_lt_one Carleson/GridStructure.lean trust unknown: Lean has no constant by this name
110. _root_.MeasureTheory.AEStronglyMeasurable.carlesonOn Carleson/Operators.lean trust unknown: Lean has no constant by this name
111. _root_.MeasureTheory.AEStronglyMeasurable.carlesonSum Carleson/Operators.lean trust unknown: Lean has no constant by this name
112. MKD Carleson/Operators.lean trust unknown: Lean has no constant by this name
113. norm_MKD_le_norm_Ks Carleson/Operators.lean trust unknown: Lean has no constant by this name
114. D0 Carleson/Psi.lean trust unknown: Lean has no constant by this name
115. D2 Carleson/Psi.lean trust unknown: Lean has no constant by this name
116. cDx0 Carleson/Psi.lean trust unknown: Lean has no constant by this name
117. le_div_ceil_mul Carleson/Psi.lean trust unknown: Lean has no constant by this name
118. one_add_logb Carleson/Psi.lean trust unknown: Lean has no constant by this name
119. eq_endpoints Carleson/Psi.lean trust unknown: Lean has no constant by this name
120. endpoint_sub_one Carleson/Psi.lean trust unknown: Lean has no constant by this name
121. sum_ψ₁ Carleson/Psi.lean trust unknown: Lean has no constant by this name
122. sum_ψ₂ Carleson/Psi.lean trust unknown: Lean has no constant by this name
123. zpow_realD_pos Carleson/Psi.lean trust unknown: Lean has no constant by this name
124. lowerBound_edist_of_Ks_ne_zero Carleson/Psi.lean trust unknown: Lean has no constant by this name
125. DoublingMeasure.volume_real_ball_two_le_same_repeat Carleson/Psi.lean trust unknown: Lean has no constant by this name
126. DoublingMeasure.volume_real_ball_two_le_same_repeat' Carleson/Psi.lean trust unknown: Lean has no constant by this name
127. DoublingMeasure.volume_ball_two_le_same_repeat' Carleson/Psi.lean trust unknown: Lean has no constant by this name
128. div_vol_le Carleson/Psi.lean trust unknown: Lean has no constant by this name
129. div_vol_le' Carleson/Psi.lean trust unknown: Lean has no constant by this name
130. div_vol_le₀ Carleson/Psi.lean trust unknown: Lean has no constant by this name
131. norm_K_le Carleson/Psi.lean trust unknown: Lean has no constant by this name
132. norm_Ks_le Carleson/Psi.lean trust unknown: Lean has no constant by this name
133. norm_Ks_le_of_dist_le Carleson/Psi.lean trust unknown: Lean has no constant by this name
134. _root_.Bornology.IsBounded.exists_bound_of_norm_Ks Carleson/Psi.lean trust unknown: Lean has no constant by this name
135. enorm_ψ_sub_ψ_le_two Carleson/Psi.lean trust unknown: Lean has no constant by this name
136. ψ_ineq Carleson/Psi.lean trust unknown: Lean has no constant by this name
137. D_pow_a_inv Carleson/Psi.lean trust unknown: Lean has no constant by this name
138. four_D_rpow_a_inv Carleson/Psi.lean trust unknown: Lean has no constant by this name
139. enorm_Ks_sub_Ks_le_close_pt1 Carleson/Psi.lean trust unknown: Lean has no constant by this name
140. enorm_Ks_sub_Ks_le_close_pt2 Carleson/Psi.lean trust unknown: Lean has no constant by this name
141. enorm_Ks_sub_Ks_le_close Carleson/Psi.lean trust unknown: Lean has no constant by this name
142. enorm_Ks_sub_Ks_le_far Carleson/Psi.lean trust unknown: Lean has no constant by this name
143. RCLike.component_one_add_neg_one Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
144. RCLike.component_I_add_neg_I Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
145. RCLike.norm_realPart_le Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
146. RCLike.norm_imPart_le Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
147. RCLike.norm_posReal_le Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
148. RCLike.norm_negReal_le Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
149. RCLike.norm_posIm_le Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
150. RCLike.norm_negIm_le Carleson/ToMathlib/Analysis/RCLike/Components.lean trust unknown: Lean has no constant by this name
151. MeasureTheory.BoundedCompactSupport._root_.isBounded_range_iff_forall_norm_le Carleson/ToMathlib/BoundedCompactSupport.lean trust unknown: Lean has no constant by this name
152. MeasureTheory.BoundedCompactSupport._root_.HasCompactSupport.star Carleson/ToMathlib/BoundedCompactSupport.lean trust unknown: Lean has no constant by this name
153. MeasureTheory.BoundedCompactSupport._root_.AEStronglyMeasurable.star Carleson/ToMathlib/BoundedCompactSupport.lean trust unknown: Lean has no constant by this name
154. MeasureTheory._root_.ENNReal.toNNReal_smul Carleson/ToMathlib/ENorm.lean trust unknown: Lean has no constant by this name
155. indicator_rpow Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
156. maximalFunction_eq_maximalFunction_one_rpow Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
157. T Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
158. T.add_le Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
159. NNReal.smul_ennreal_eq_mul Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
160. T.smul Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
161. measure_biUnion_le_lintegral_aux Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
162. tr Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
163. tr_mono Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
164. tr_union Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
165. MeasureTheory.MemLp.maximalFunction_lt_top Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
166. hasStrongType_maximalFunction_top Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
167. hasWeakType_maximalFunction_one Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
168. sublinearOn_maximalFunction_one Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
169. hasWeakType_maximalFunction_equal_exponents Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
170. maximalFunction_ae_lt_top Carleson/ToMathlib/HardyLittlewood.lean trust unknown: Lean has no constant by this name
171. _root_.MeasureTheory.Integrable.conj Carleson/ToMathlib/MeasureTheory/Function/L1Integrable.lean trust unknown: Lean has no constant by this name
172. _root_.MeasureTheory.Integrable.mul_conj Carleson/ToMathlib/MeasureTheory/Function/L1Integrable.lean trust unknown: Lean has no constant by this name
173. MeasureTheory.SimpleFunc.helper Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean trust unknown: Lean has no constant by this name
174. r_sub_p_nonneg Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
175. ENNReal.eLpNorm_eq_eLpNorm_rpow Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
176. ENNReal.convolution_zero_of_c_nonpos Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
177. ENNReal.eLpNorm_top_convolution_le_aux Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
178. ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm_aux Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
179. ENNReal.eLpNorm_convolution_le_ofReal_aux Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
180. ENNReal.eLpNorm_convolution_le_of_norm_le_mul_aux Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean trust unknown: Lean has no constant by this name
181. _root_.ENNReal.nnorm_toReal Carleson/ToMathlib/Misc.lean trust unknown: Lean has no constant by this name
182. MeasureTheory._root_.AEMeasurable.piecewise Carleson/ToMathlib/Misc.lean trust unknown: Lean has no constant by this name
183. MeasureTheory._root_.AEMeasurable.ite Carleson/ToMathlib/Misc.lean trust unknown: Lean has no constant by this name
184. ComputationsChoiceExponent.one_sub_ioo_toReal Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean trust unknown: Lean has no constant by this name
185. MeasureTheory._root_.ContinuousLinearMap.distribution_le Carleson/ToMathlib/WeakType.lean trust unknown: Lean has no constant by this name
186. maximal_theorem' Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
187. maximal_theorem'' Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
188. isFiniteMeasure_of_not_generalCase Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
189. czBall_subset_czBall Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
190. MeasurableSet.czPartition Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
191. czPartition_subset_czBall7 Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
192. czPartition_pairwise_disjoint_on Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
193. globalMaximalFunction_preimage_finite Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
194. volume_czPartition_lt_top Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
195. volume_czBall7_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
196. volume_czBall3_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
197. laverage_czBall7_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
198. lintegral_czPartition_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
199. czRemainder'_eq_zero Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
200. α_le_mul_α Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
201. enorm_czApproximation_le_finite Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
202. eLpNorm_czApproximation_le_finite Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
203. eLpNorm_czApproximation_le_infinite Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
204. ineq_10_2_32 Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
205. eLpNorm_restrict_czRemainder'_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
206. eLpNorm_czRemainder_le' Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
207. czBall3_subset_of_mem_Ω Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
208. six_mul_czRadius_le_of_mem_Ω Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
209. α'_pos Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
210. div_α'_eq Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
211. czOperatorBoundSummand Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
212. czOperatorBound_eq Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
213. 𝒥₁ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
214. 𝒥₂ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
215. 𝒥₃ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
216. union_𝒥 Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
217. lemma_10_2_7_bound' Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
218. lemma_10_2_7_bound Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
219. 𝒥₁_bound Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
220. tsum_𝒥₁ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
221. d Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
222. integrableOn_d Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
223. enorm_d_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
224. g₀ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
225. g Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
226. integrableOn_g₀ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
227. lintegral_enorm_g₀_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
228. integrableOn_g Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
229. integral_g Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
230. lintegral_enorm_half_g Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
231. 𝒥₂_bound Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
232. A Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
233. A_subset Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
234. sum_volume_restrict_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
235. tsum_integral_K_le Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
236. tsum_𝒥₂ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
237. tsum_𝒥₃ Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
238. czOperator_czRemainder' Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name
239. czOperator_czRemainder Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean trust unknown: Lean has no constant by this name

Depend on sorry (27)

1. exceptional_set_carleson Carleson/Classical/CarlesonHunt.lean
2. carleson_hunt_interval Carleson/Classical/CarlesonHunt.lean
3. carleson_hunt_real Carleson/Classical/CarlesonHunt.lean
4. classical_carleson_from_carleson_hunt_real Carleson/Classical/CarlesonHunt.lean
5. carleson_hunt_two_pi Carleson/Classical/CarlesonHunt.lean
6. carleson_hunt' Carleson/Classical/CarlesonHunt.lean
7. carleson_hunt Carleson/Classical/CarlesonHunt.lean
8. general_carlesonOperator_on_the_reals_hasStrongType Carleson/Classical/CarlesonOnTheRealLine.lean
9. rcarleson' Carleson/Classical/CarlesonOnTheRealLine.lean
10. rcarleson'_restrict Carleson/Classical/ControlApproximationEffect.lean
11. C_distribution_carlesonOperatorReal_le Carleson/Classical/ControlApproximationEffect.lean
12. C_distribution_carlesonOperatorReal_le_pos Carleson/Classical/ControlApproximationEffect.lean
13. distribution_carlesonOperatorReal_le Carleson/Classical/ControlApproximationEffect.lean
14. C_control_approximation_effect Carleson/Classical/ControlApproximationEffect.lean
15. C_control_approximation_effect_pos Carleson/Classical/ControlApproximationEffect.lean
16. C_control_approximation_effect_property Carleson/Classical/ControlApproximationEffect.lean
17. C_control_approximation_effect_le Carleson/Classical/ControlApproximationEffect.lean
18. control_approximation_effect Carleson/Classical/ControlApproximationEffect.lean
19. C_LorentzInterpolation Carleson/ToMathlib/RealInterpolation/LorentzInterpolation.lean
20. C_LorentzInterpolation_pos Carleson/ToMathlib/RealInterpolation/LorentzInterpolation.lean
21. exists_hasLorentzType_real_interpolation Carleson/ToMathlib/RealInterpolation/LorentzInterpolation.lean
22. C_carleson_hasStrongType Carleson/TwoSidedCarleson/RestrictedWeakType.lean
23. C_carleson_hasStrongType_pos Carleson/TwoSidedCarleson/RestrictedWeakType.lean
24. two_sided_metric_carleson_hasStrongType Carleson/TwoSidedCarleson/RestrictedWeakType.lean
25. classical_carleson' Challenge.lean
26. metric_carleson'' Challenge.lean
27. linearized_metric_carleson' Challenge.lean