`Carleson/Operators.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

34 declarations, 0 contain sorry, 0 declared as axioms

Carleson operators

Imports (3)

Imported by 4 files

lemma bcs_of_measurable_of_le_indicator_f line 22 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Measurable, NNReal, defaultA, LE.le, Norm.norm, Set.indicator, OfNat.ofNat, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume
Proof uses: MeasureTheory.BoundedCompactSupport.indicator_of_isCompact_closure, MeasureTheory.memLp_top_const, Bornology.IsBounded.isCompact_closure, ProofData.isBounded_F, ProofData.measurableSet_F, MeasureTheory.BoundedCompactSupport.mono_norm, Measurable.aestronglyMeasurable
80 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma bcs_of_measurable_of_le_indicator_g line 29 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Measurable, NNReal, defaultA, LE.le, Norm.norm, Set.indicator, OfNat.ofNat, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume
Proof uses: MeasureTheory.BoundedCompactSupport.indicator_of_isCompact_closure, MeasureTheory.memLp_top_const, Bornology.IsBounded.isCompact_closure, ProofData.isBounded_G, ProofData.measurableSet_G, MeasureTheory.BoundedCompactSupport.mono_norm, Measurable.aestronglyMeasurable
80 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def carlesonOn The operator T_𝔭 defined in Proposition 2.0.2 line 39 source
Source documentation
The operator T_𝔭 defined in Proposition 2.0.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓
Proof uses: Set.indicator, E, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Ks, 𝔰
43 instances, coercions and auxiliary constants left out.
```
def carlesonOn (p : 𝔓 X) (f : X → ℂ) : X → ℂ :=
…
```
Mentions: 𝔓
lemma measurable_carlesonOn Documented declaration: measurable_carlesonOn line 46 source
Source comment
Deprecated for `AEStronglyMeasurable.carlesonOn` Used through `measurable_carlesonSum` in `Antichain.AntichainOperator` and `ForestOperator.Forests` with nontrivial rework in order to move from `Measurable` to `AEStronglyMeasurable`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, carlesonOn
Proof uses: Measurable.indicator, E, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Ks, 𝔰, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.integral_prod_right, Measurable.stronglyMeasurable, Prod, Function.uncurry, Measurable.fun_mul, Prod.fst, Prod.snd and 13 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma measurable_carlesonOn {p : 𝔓 X} {f : X → ℂ} (measf : Measurable f) :
    Measurable (carlesonOn p f) := by
…
```
Mentions: 𝔓, carlesonOn
def carlesonSum The operator T_ℭ f defined at the bottom of Section 7.4 line 54 source
Source documentation
The operator T_ℭ f defined at the bottom of Section 7.4. We will use this in other places of the formalization as well.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓
Proof uses: Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, carlesonOn
27 instances, coercions and auxiliary constants left out.
```
def carlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: ℭ, 𝔓
lemma measurable_carlesonSum line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, carlesonSum
Proof uses: Finset.measurable_sum, carlesonOn, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Finset, measurable_carlesonOn
62 instances, coercions and auxiliary constants left out.
lemma _root_.MeasureTheory.AEStronglyMeasurable.carlesonOn line 62 source
lemma _root_.MeasureTheory.AEStronglyMeasurable.carlesonSum line 70 source
lemma carlesonOn_def' line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Eq, carlesonOn, Set.indicator, E and 10 more
Proof uses: congr_arg, funext, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 5 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma support_carlesonOn_subset_E line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, Function.support, carlesonOn, E
Proof uses: Membership.mem, Set.mem_of_indicator_ne_zero, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Ks, 𝔰
46 instances, coercions and auxiliary constants left out.
lemma support_carlesonSum_subset line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, Function.support, carlesonSum, Set.iUnion and 2 more
Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, Eq, OfNat.ofNat, Not, Finset.sum_eq_zero, Finset.filter, Classical.propDecidable, Finset.univ, carlesonOn, Finset, Iff.mp, Function.notMem_support, Set.mem_biUnion, And.right, Eq.mp, And, E_subset_𝓘, support_carlesonOn_subset_E, Ne, congrArg and 2 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonOn line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, BddAbove, Set.range and 2 more
Proof uses: Classical.choice, inferInstance, Nonempty, And, LT.lt, OfNat.ofNat, LE.le, tsupport, Metric.closedBall, Exists, Bornology.IsBounded.subset_closedBall_lt, IsCompact.isBounded, MeasureTheory.BoundedCompactSupport.hasCompactSupport, HAdd.hAdd, HDiv.hDiv, HPow.hPow, 𝔰, Function.support, Eq.mpr, Set.indicator and 95 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.carlesonOn line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, carlesonOn
Proof uses: MeasureTheory.BoundedCompactSupport.mk, Membership.mem, Set.range, Norm.norm, LE.le, Exists, MeasureTheory.MemLp, Top.top, ENNReal, Iff.mp, BddAbove, bddAbove_def, MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonOn, MeasureTheory.memLp_top_of_bound, MeasureTheory.AEStronglyMeasurable.carlesonOn, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.ae, MeasureTheory.Measure, Eq.mp and 20 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonSum line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, BddAbove, Set.range and 2 more
Proof uses: BddAbove.range_mono, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, carlesonOn, norm_sum_le, BddAbove.range_finsetSum, LE.le, Finset, MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonOn
74 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.carlesonSum line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, carlesonSum
Proof uses: MeasureTheory.BoundedCompactSupport.finset_sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, carlesonOn, Finset, MeasureTheory.BoundedCompactSupport.carlesonOn
63 instances, coercions and auxiliary constants left out.
lemma carlesonSum_inter_add_inter_compl line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Eq, HAdd.hAdd, carlesonSum, Inter.inter and 1 more
Proof uses: id, Eq.mpr, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, carlesonOn, Not, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Finset.sum_filter_add_sum_filter_not, HAdd, AddCommMonoid, Finset, Finset.ext, of_eq_true and 9 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma sum_carlesonSum_of_pairwiseDisjoint line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Finset, Set.PairwiseDisjoint, Eq, Finset.sum and 3 more
Proof uses: id, Eq.mpr, Finset.filter, Classical.propDecidable, Finset.univ, carlesonOn, Finset.biUnion, congrArg, Eq.symm, Finset.sum_biUnion, propext, Iff.intro, Ne, Function.onFun, Disjoint, eq_of_heq, PartialOrder, OrderBot, HEq, Eq.refl and 22 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
def adjointCarleson The definition of Tₚ*g(x), defined above Lemma 7.4.1 line 210 source
Source documentation
The definition of Tₚ*g(x), defined above Lemma 7.4.1

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓
Proof uses: MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, E, HMul.hMul, RingHom, starRingEnd, Ks, 𝔰, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc
48 instances, coercions and auxiliary constants left out.
```
def adjointCarleson (p : 𝔓 X) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: 𝔓
def adjointCarlesonSum The definition of T_ℭ*g(x), defined at the bottom of Section 7.4 line 215 source
Source documentation
The definition of T_ℭ*g(x), defined at the bottom of Section 7.4

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓
Proof uses: Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, adjointCarleson
29 instances, coercions and auxiliary constants left out.
```
def adjointCarlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: ℭ, 𝔓
lemma adjointCarlesonSum_inter A helper lemma used in Lemma 7.5.10 line 219 source
Source documentation
A helper lemma used in Lemma 7.5.10.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Eq, adjointCarlesonSum, Inter.inter, HSub.hSub and 1 more
Proof uses: id, Eq.symm, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, adjointCarleson, Eq.mpr, HAdd.hAdd, congrArg, propext, sub_eq_iff_eq_add, Union.union, Finset, Finset.sum_union, Disjoint, Eq.trans, Not, forall_congr and 18 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma adjointCarlesonSum_inter {A B : Set (𝔓 X)} {f : X → ℂ} {x : X} :
    adjointCarlesonSum (A ∩ B) f x = adjointCarlesonSum A f x - adjointCarlesonSum (A \ B) f x := by
…
```
Mentions: A, 𝔓, adjointCarlesonSum
lemma adjoint_eq_adjoint_indicator line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, E, 𝓘, Eq and 2 more
Proof uses: funext, MeasureTheory.setIntegral_congr_fun, HMul.hMul, RingHom, starRingEnd, Ks, 𝔰, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, MeasureTheory.MeasureSpace.volume, measurableSet_E, Membership.mem, HMul, Eq.rec, Eq.refl, Eq.symm, Set.indicator_of_mem
57 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.StronglyMeasurable.adjointCarleson line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.StronglyMeasurable, adjointCarleson
Proof uses: MeasureTheory.StronglyMeasurable.integral_prod_right', MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, E, Prod, HMul.hMul, RingHom, starRingEnd, Ks, 𝔰, Prod.snd, Prod.fst, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, MeasureTheory.StronglyMeasurable.mul, Continuous.comp_stronglyMeasurable, Complex.continuous_conj and 16 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.adjointCarleson line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, adjointCarleson
Proof uses: MeasureTheory.AEStronglyMeasurable.integral_prod_right', MeasureTheory.Measure.restrict, E, Prod, HMul.hMul, RingHom, starRingEnd, Ks, 𝔰, Prod.snd, Prod.fst, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.Measure.prod, MeasureTheory.Measure.AbsolutelyContinuous.prod, MeasureTheory.Measure.AbsolutelyContinuous.rfl and 20 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.StronglyMeasurable.adjointCarlesonSum line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.StronglyMeasurable, adjointCarlesonSum
Proof uses: id, Finset.stronglyMeasurable_fun_sum, adjointCarleson, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Finset, MeasureTheory.StronglyMeasurable.adjointCarleson
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.adjointCarlesonSum line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, adjointCarlesonSum
Proof uses: id, Finset.aestronglyMeasurable_fun_sum, adjointCarleson, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Finset, MeasureTheory.AEStronglyMeasurable.adjointCarleson
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarleson line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, BddAbove, Set.range and 2 more
Proof uses: And, LE.le, OfNat.ofNat, Membership.mem, tsupport, Ks, 𝔰, Exists, Bornology.IsBounded.exists_bound_of_norm_Ks, IsCompact.isBounded, MeasureTheory.BoundedCompactSupport.hasCompactSupport, HMul.hMul, ENNReal.toReal, MeasureTheory.eLpNorm, Top.top, ENNReal, MeasureTheory.Measure.real, E, Exists.intro, upperBounds and 40 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.adjointCarleson line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, adjointCarleson
Proof uses: MeasureTheory.BoundedCompactSupport.mk, Membership.mem, upperBounds, Set.range, Norm.norm, BddAbove, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarleson, MeasureTheory.memLp_top_of_bound, MeasureTheory.AEStronglyMeasurable.adjointCarleson, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, Filter.Eventually.of_forall, LE.le, MeasureTheory.ae, MeasureTheory.Measure, Eq.mp, Eq.trans, Eq and 56 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarlesonSum line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, BddAbove, Set.range and 2 more
Proof uses: BddAbove.range_mono, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, adjointCarleson, norm_sum_le, BddAbove.range_finsetSum, LE.le, Finset, MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarleson
76 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.adjointCarlesonSum line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, adjointCarlesonSum
Proof uses: id, MeasureTheory.BoundedCompactSupport.finset_sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, adjointCarleson, Finset, MeasureTheory.BoundedCompactSupport.adjointCarleson
65 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
abbrev MKD MKD is short for "modulated kernel times dilated bump" line 330 source
Source documentation
MKD is short for "modulated kernel times dilated bump".
```
private abbrev MKD (s : ℤ) x y := exp (I * (Q x y - Q x x)) * Ks s x y (K := K)
…
```
Mentions: s, Ks, K
lemma norm_MKD_le_norm_Ks line 333 source
lemma adjointCarleson_adjoint adjointCarleson is the adjoint of carlesonOn line 337 source
Source documentation
adjointCarleson is the adjoint of carlesonOn.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, 𝔓, Eq, MeasureTheory.integral and 5 more
Proof uses: Set.indicator, E, OfNat.ofNat, 𝔰, MeasureTheory.Integrable, Prod, Function.uncurry, Norm.norm, And, LE.le, Membership.mem, tsupport, Ks, Exists, Bornology.IsBounded.exists_bound_of_norm_Ks, IsCompact.isBounded, MeasureTheory.BoundedCompactSupport.hasCompactSupport, dite, Classical.propDecidable, id and 165 more
291 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
```
lemma adjointCarleson_adjoint
    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (p : 𝔓 X) :
    ∫ x, conj (g x) * carlesonOn p f x = ∫ y, conj (adjointCarleson p g y) * f y := by
…
```
Mentions: g, 𝔓, carlesonOn, adjointCarleson
lemma adjointCarlesonSum_adjoint adjointCarlesonSum is the adjoint of carlesonSum line 406 source
Source documentation
adjointCarlesonSum is the adjoint of carlesonSum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, 𝔓, Eq, MeasureTheory.integral and 5 more
Proof uses: id, Eq.mpr, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, carlesonOn, congrFun', congrArg, funext, Finset.mul_sum, Trans.trans, adjointCarleson, MeasureTheory.integral_finsetSum, Finset, MeasureTheory.BoundedCompactSupport.integrable_fun_mul, MeasureTheory.BoundedCompactSupport.starRingEnd, MeasureTheory.BoundedCompactSupport.integrable, MeasureTheory.BoundedCompactSupport.carlesonOn and 20 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma adjointCarlesonSum_adjoint
    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (ℭ : Set (𝔓 X)) :
    ∫ x, conj (g x) * carlesonSum ℭ f x = ∫ x, conj (adjointCarlesonSum ℭ g x) * f x := by
…
```
Mentions: g, ℭ, 𝔓, carlesonSum, adjointCarlesonSum
lemma integrable_adjointCarlesonSum line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, MeasureTheory.Integrable, adjointCarlesonSum
Proof uses: MeasureTheory.BoundedCompactSupport.integrable, MeasureTheory.BoundedCompactSupport.adjointCarlesonSum
72 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.