BoundedCompactSupport.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

44 declarations, 0 contain sorry, 0 declared as axioms

Bounded compactly supported functions

The purpose of this file is to provide helper lemmas to streamline proofs that functions are bounded, compactly supported and measurable.

Most functions we need to deal with are of this class. This can be a useful way to streamline proofs of L^p membership, in particular integrability.

Todo: make Mathlib.Tactic.FunProp work for this

This can be expanded as needed

Upstreaming status: should be upstreamed, but need to clarify design questions first

want to tag this with fun_prop first and make it work smoothly (see #499)
this is similar to BoundedFiniteSupport (and in almost all cases, implies the latter) TODO: are there any advantages of using this and not BoundedFiniteSupport? for instance, is there any operation which preserves BoundedCompactSupport but not BoundedFiniteSupport? Decide if we want both classes in mathlib or just one of them. If the latter, rewrite all of Carleson/ToMathlib to use that one class. (Discussion on Zulip, Result: keep both here, but upstream only BoundedCompactSupport)

Imports (2)

Imported by 3 files

theorem MeasureTheory.eLpNorm_mono_ac line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.Measure.AbsolutelyContinuous, LE.le, ENNReal, MeasureTheory.eLpNorm, Top.top
Proof uses: Eq.mpr, MeasureTheory.eLpNormEssSup, id, Eq, congr, congrArg, MeasureTheory.eLpNorm_exponent_top, of_eq_true, eq_true, MeasureTheory.eLpNormEssSup_mono_measure
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.MemLp.mono_ac line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.Measure.AbsolutelyContinuous
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLpNorm, MeasureTheory.AEStronglyMeasurable.mono_ac, And.left, LE.le.trans_lt, MeasureTheory.eLpNorm_mono_ac, And.right
7 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.MemLp.comp_quasiMeasurePreserving line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.Measure.QuasiMeasurePreserving, Function.comp
Proof uses: MeasureTheory.MemLp.comp_of_map, MeasureTheory.MemLp.mono_ac, MeasureTheory.Measure.map, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable
4 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.MemLp.ae_norm_le line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.MemLp, Top.top, ENNReal, Filter.Eventually, LE.le, Real, Norm.norm, ENNReal.toReal, MeasureTheory.eLpNorm, MeasureTheory.ae
Proof uses: Filter.mp_mem, Set.ofPred, ENorm.enorm, MeasureTheory.eLpNormEssSup, MeasureTheory.ae_le_eLpNormEssSup, Filter.univ_mem', Membership.mem, Set, id, Eq.mpr, Eq, congrFun', congrArg, ENNReal.toReal_mono, LT.lt.ne, And.right, MeasureTheory.AEStronglyMeasurable, LT.lt, of_eq_true, Eq.trans and 3 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
structure MeasureTheory.BoundedCompactSupport Bounded compactly supported measurable functions line 84 source
Source documentation
Bounded compactly supported measurable functions

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, ENorm, Zero, autoParam, MeasureTheory.Measure
1 instances, coercions and auxiliary constants left out.
```
structure BoundedCompactSupport (f : X → E) (μ : Measure X := by volume_tac) :
…
```
Mentions: E
lemma MeasureTheory.BoundedCompactSupport._root_.isBounded_range_iff_forall_norm_le line 94 source
theorem MeasureTheory.BoundedCompactSupport.aestronglyMeasurable line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, ENorm, Zero, MeasureTheory.BoundedCompactSupport, MeasureTheory.AEStronglyMeasurable
Proof uses: MeasureTheory.MemLp.aestronglyMeasurable, Top.top, ENNReal, MeasureTheory.BoundedCompactSupport.memLp_top
1 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.boundedFiniteSupport line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, ENorm, Zero, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.BoundedCompactSupport, BoundedFiniteSupport
Proof uses: BoundedFiniteSupport.mk, MeasureTheory.BoundedCompactSupport.memLp_top, LE.le.trans_lt, ENNReal, autoParam, Set, Function.support, tsupport, Top.top, MeasureTheory.measure_mono, subset_tsupport, IsCompact.measure_lt_top, HasCompactSupport.isCompact, MeasureTheory.BoundedCompactSupport.hasCompactSupport
7 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.mono_ac line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, ContinuousENorm, Zero, MeasureTheory.BoundedCompactSupport, MeasureTheory.Measure.AbsolutelyContinuous
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.mono_ac, MeasureTheory.BoundedCompactSupport.memLp_top, MeasureTheory.BoundedCompactSupport.hasCompactSupport
2 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.mono_measure line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, ContinuousENorm, Zero, MeasureTheory.BoundedCompactSupport, LE.le
Proof uses: MeasureTheory.BoundedCompactSupport.mono_ac, LE.le.absolutelyContinuous
8 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.restrict line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, ContinuousENorm, Zero, Set, MeasureTheory.BoundedCompactSupport, MeasureTheory.Measure.restrict
Proof uses: MeasureTheory.BoundedCompactSupport.mono_measure, MeasureTheory.Measure.restrict_le_self
2 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.memLp Bounded compactly supported functions are in all Lᵖ spaces line 136 source
Source documentation
Bounded compactly supported functions are in all Lᵖ spaces.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, ESeminormedAddCommMonoid, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.BoundedCompactSupport, ENNReal, MeasureTheory.MemLp
Proof uses: BoundedFiniteSupport.memLp, MeasureTheory.BoundedCompactSupport.boundedFiniteSupport
16 instances, coercions and auxiliary constants left out.
```
theorem memLp [IsFiniteMeasureOnCompacts μ] (hf : BoundedCompactSupport f μ) (p : ℝ≥0∞) :
    MemLp f p μ :=
…
```
Mentions: MeasureTheory.BoundedCompactSupport
theorem MeasureTheory.BoundedCompactSupport.integrable Bounded compactly supported functions are integrable line 150 source
Source documentation
Bounded compactly supported functions are integrable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.BoundedCompactSupport, MeasureTheory.Integrable
Proof uses: BoundedFiniteSupport.integrable, MeasureTheory.BoundedCompactSupport.boundedFiniteSupport
28 instances, coercions and auxiliary constants left out.
```
theorem integrable [IsFiniteMeasureOnCompacts μ] (hf : BoundedCompactSupport f μ) :
    Integrable f μ :=
…
```
Mentions: MeasureTheory.BoundedCompactSupport
theorem MeasureTheory.BoundedCompactSupport.zero line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, OfNat.ofNat
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.memLp_top_const, HasCompactSupport.zero
30 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.enorm line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, ENNReal, ENorm.enorm
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.enorm, Top.top, MeasureTheory.BoundedCompactSupport.memLp_top, Iff.mpr, HasCompactSupport, Function.comp, hasCompactSupport_comp_left, enorm_eq_zero, MeasureTheory.BoundedCompactSupport.hasCompactSupport
38 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.norm preferably use enorm line 166 source
Source comment
preferably use `enorm`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, Real, Norm.norm
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.norm, Top.top, ENNReal, MeasureTheory.BoundedCompactSupport.memLp_top, Iff.mpr, HasCompactSupport, Function.comp, hasCompactSupport_comp_left, norm_eq_zero, MeasureTheory.BoundedCompactSupport.hasCompactSupport
46 instances, coercions and auxiliary constants left out.
```
theorem norm (hf : BoundedCompactSupport f μ) : BoundedCompactSupport (‖f ·‖) μ where
…
```
Mentions: MeasureTheory.BoundedCompactSupport
theorem MeasureTheory.BoundedCompactSupport.comp_left_norm line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, Eq, OfNat.ofNat, Continuous, Real, Norm.norm, Function.comp
Proof uses: MeasureTheory.BoundedCompactSupport.mk, Eq.mpr, MeasureTheory.MemLp, Top.top, ENNReal, id, congrArg, Eq.symm, propext, MeasureTheory.memLp_norm_iff, Continuous.comp_aestronglyMeasurable, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, congrFun', autoParam, funext, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.comp_left, MeasureTheory.BoundedCompactSupport.hasCompactSupport
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.neg line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, Neg.neg
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.neg, Top.top, ENNReal, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.neg, MeasureTheory.BoundedCompactSupport.hasCompactSupport
33 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.add line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, HAdd.hAdd
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.add, Top.top, ENNReal, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.add, MeasureTheory.BoundedCompactSupport.hasCompactSupport
50 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.sub line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, HSub.hSub
Proof uses: Eq.mpr, HAdd.hAdd, Neg.neg, id, Eq, congrArg, sub_eq_add_neg, MeasureTheory.BoundedCompactSupport.add, MeasureTheory.BoundedCompactSupport.neg
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.mul_bdd_right line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, MeasureTheory.MemLp, Top.top, ENNReal, HMul.hMul
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.mul, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.mul_right, MeasureTheory.BoundedCompactSupport.hasCompactSupport
54 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.mul_bdd_left line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, MeasureTheory.MemLp, Top.top, ENNReal, HMul.hMul
Proof uses: Eq.mpr, id, Eq, congrArg, mul_comm, MeasureTheory.BoundedCompactSupport.mul_bdd_right
59 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.mul line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, HMul.hMul
Proof uses: MeasureTheory.BoundedCompactSupport.mul_bdd_right, MeasureTheory.BoundedCompactSupport.memLp_top
46 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.integrable_mul doesn't use compact support but is convenient to have here line 219 source
Source comment
doesn't use compact support but is convenient to have here

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, MeasureTheory.Integrable, HMul.hMul
Proof uses: Eq.mpr, MeasureTheory.MemLp, OfNat.ofNat, ENNReal, id, Eq, congrArg, Eq.symm, propext, MeasureTheory.memLp_one_iff_integrable, MeasureTheory.MemLp.mul, Top.top, Eq.mp, MeasureTheory.BoundedCompactSupport.memLp_top
56 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem integrable_mul (hf : BoundedCompactSupport f μ) (hg : Integrable g μ) :
    Integrable (f * g) μ := by
…
```
Mentions: MeasureTheory.BoundedCompactSupport, g
theorem MeasureTheory.BoundedCompactSupport.integrable_fun_mul line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, MeasureTheory.Integrable, HMul.hMul
Proof uses: MeasureTheory.BoundedCompactSupport.integrable_mul
45 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.BoundedCompactSupport._root_.HasCompactSupport.star line 231 source
lemma MeasureTheory.BoundedCompactSupport._root_.AEStronglyMeasurable.star line 236 source
lemma MeasureTheory.BoundedCompactSupport.eLpNorm_star line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, RCLike, Eq, ENNReal, MeasureTheory.eLpNorm, Star.star, Top.top
Proof uses: id, Eq.mpr, congrArg, MeasureTheory.eLpNorm_congr_enorm_ae, of_eq_true, Filter.Eventually, ENorm.enorm, MeasureTheory.ae, Eq.trans, True, congrFun', Filter, funext, RCLike.enorm_conj, eq_self, Eq.refl
57 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.conj line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, Star.star
Proof uses: MeasureTheory.BoundedCompactSupport.mk, And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, ENNReal, MeasureTheory.eLpNorm, Top.top, MeasureTheory.AEStronglyMeasurable.star, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, Eq.mpr, id, Eq, congrArg, MeasureTheory.BoundedCompactSupport.eLpNorm_star, MeasureTheory.MemLp, MeasureTheory.BoundedCompactSupport.memLp_top, Ne.lt_top, MeasureTheory.MemLp.eLpNorm_ne_top, HasCompactSupport.star, MeasureTheory.BoundedCompactSupport.hasCompactSupport
72 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem 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 line 257 source
Source comment
This lemma is defeq to `BoundedCompactSupport.conj`, but `starRingEnd` and `conj` are both simp normal forms, so a lemma for each is needed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, RingHom, starRingEnd
Proof uses: MeasureTheory.BoundedCompactSupport.conj
48 instances, coercions and auxiliary constants left out.
```
theorem starRingEnd (hf : BoundedCompactSupport f μ) :
  BoundedCompactSupport (fun x ↦ (starRingEnd 𝕜) (f x)) μ := hf.conj
…
```
Mentions: MeasureTheory.BoundedCompactSupport
theorem MeasureTheory.BoundedCompactSupport.const_mul line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, HMul.hMul
Proof uses: MeasureTheory.BoundedCompactSupport.mul_bdd_left, MeasureTheory.memLp_top_const
48 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.mul_const line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, HMul.hMul
Proof uses: MeasureTheory.BoundedCompactSupport.mul_bdd_right, MeasureTheory.memLp_top_const
48 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.mono If ‖f‖ is bounded by g and g is bounded compactly supported, then so is f line 273 source
Source documentation
If ‖f‖ is bounded by g and g is bounded compactly supported, then so is f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, ENNReal, MeasureTheory.BoundedCompactSupport, MeasureTheory.AEStronglyMeasurable, LE.le, ENorm.enorm
Proof uses: MeasureTheory.BoundedCompactSupport.mk, And.intro, LT.lt, MeasureTheory.eLpNorm, Top.top, LE.le.trans_lt, MeasureTheory.eLpNorm_mono_enorm, MeasureTheory.MemLp.eLpNorm_lt_top, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.mono, MeasureTheory.BoundedCompactSupport.hasCompactSupport, Classical.byContradiction, Set, Function.support, Not, Exists, Eq, OfNat.ofNat, False, Eq.mp and 13 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem mono {g : X → ℝ≥0∞} (hg : BoundedCompactSupport g μ) (hf : AEStronglyMeasurable f μ)
    (hfg : ∀ x, ‖f x‖ₑ ≤ g x) : BoundedCompactSupport f μ where
…
```
Mentions: g, MeasureTheory.BoundedCompactSupport
theorem MeasureTheory.BoundedCompactSupport.mono_norm use mono preferably line 285 source
Source comment
use `mono` preferably

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, Real, MeasureTheory.BoundedCompactSupport, MeasureTheory.AEStronglyMeasurable, LE.le, Norm.norm
Proof uses: MeasureTheory.BoundedCompactSupport.mk, And.intro, LT.lt, ENNReal, MeasureTheory.eLpNorm, Top.top, LE.le.trans_lt, MeasureTheory.eLpNorm_mono_real, MeasureTheory.MemLp.eLpNorm_lt_top, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.mono, MeasureTheory.BoundedCompactSupport.hasCompactSupport, Classical.byContradiction, Set, Function.support, Not, Exists, Eq, OfNat.ofNat, False and 14 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem mono_norm {g : X → ℝ} (hg : BoundedCompactSupport g μ) (hf : AEStronglyMeasurable f μ)
    (hfg : ∀ x, ‖f x‖ ≤ g x) : BoundedCompactSupport f μ where
…
```
Mentions: g, MeasureTheory.BoundedCompactSupport
theorem MeasureTheory.BoundedCompactSupport.toComplex line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, Real, MeasureTheory.BoundedCompactSupport, Complex
Proof uses: MeasureTheory.BoundedCompactSupport.mono, ENorm.enorm, MeasureTheory.BoundedCompactSupport.enorm, Continuous.comp_aestronglyMeasurable, Complex.continuous_ofReal, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, of_eq_true, LE.le, ENNReal, Eq.trans, True, forall_congr, ENNReal.ofReal, abs, congr, congrArg, Norm.norm, Complex.norm_real, implies_true
51 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.finset_sum A finite sum of bounded compactly supported functions is bounded compactly supported line 309 source
Source documentation
A finite sum of bounded compactly supported functions is bounded compactly supported.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, Finset, Membership.mem, MeasureTheory.BoundedCompactSupport, Finset.sum
Proof uses: Finset.induction, Classical.propDecidable, Eq, EmptyCollection.emptyCollection, of_eq_true, OfNat.ofNat, Not, Insert.insert, Eq.mpr, HAdd.hAdd, id, congrFun', congrArg, autoParam, funext, AddCommMonoid, Finset.sum_insert, MeasureTheory.BoundedCompactSupport.add, Finset.mem_insert_self, Finset.mem_insert_of_mem
44 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem finset_sum
    (hF : ∀ i ∈ s, BoundedCompactSupport (F i) μ) :
    BoundedCompactSupport (fun x ↦ ∑ i ∈ s, F i x) μ := by
…
```
Mentions: s, MeasureTheory.BoundedCompactSupport
lemma MeasureTheory.BoundedCompactSupport.sq_eLpNorm_le_sums Used in Proposition 2.0.4 line 323 source
Source documentation
Used in Proposition 2.0.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasureOnCompacts, Complex, MeasureTheory.BoundedCompactSupport, Finset, LE.le, ENNReal, HPow.hPow, Nat, MeasureTheory.eLpNorm, Finset.sum, OfNat.ofNat, HAdd.hAdd, Finset.filter, Ne, Eq, Classical.propDecidable, ENorm.enorm and 5 more
Proof uses: MeasureTheory.Integrable, MeasureTheory.BoundedCompactSupport.integrable, Star.star, MeasureTheory.BoundedCompactSupport.mul, MeasureTheory.BoundedCompactSupport.conj, Trans.trans, MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj, MeasureTheory.BoundedCompactSupport.memLp, MeasureTheory.BoundedCompactSupport.finset_sum, Membership.mem, eq_of_heq, ENorm, HEq, Eq.refl, HEq.refl, Eq.symm, NormedAddCommGroup, NormedSpace, funext, Eq.mpr and 15 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma sq_eLpNorm_le_sums [IsFiniteMeasureOnCompacts μ] {f : ι → X → ℂ}
    (hf : ∀ i, BoundedCompactSupport (f i) μ) {s : Finset ι} :
    eLpNorm (∑ i ∈ s, f i ·) 2 μ ^ 2 ≤
    ∑ i ∈ s, eLpNorm (f i) 2 μ ^ 2 +
    ∑ i ∈ s, ∑ j ∈ s with i ≠ j, ‖∫ x, f i x * conj (f j x) ∂μ‖ₑ := by
…
```
Mentions: MeasureTheory.BoundedCompactSupport, s, MeasureTheory.BoundedCompactSupport.conj
theorem MeasureTheory.BoundedCompactSupport.prod_mul An elementary tensor of bounded compactly supported functions is bounded compactly supported line 367 source
Source documentation
An elementary tensor of bounded compactly supported functions is bounded compactly supported.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, RCLike, MeasureTheory.MeasureSpace, R1Space, Prod, MeasureTheory.BoundedCompactSupport, Function.uncurry, HMul.hMul, MeasureTheory.Measure.prod
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp, Prod.fst, Top.top, ENNReal, MeasureTheory.MemLp.comp_quasiMeasurePreserving, MeasureTheory.BoundedCompactSupport.memLp_top, MeasureTheory.Measure.quasiMeasurePreserving_fst, Prod.snd, MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.MemLp.mul, HasCompactSupport.intro, SProd.sprod, Set, tsupport, IsCompact.prod, MeasureTheory.BoundedCompactSupport.hasCompactSupport, Not, Membership.mem, Eq and 14 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem prod_mul (hf : BoundedCompactSupport f μ) (hg : BoundedCompactSupport g ν) :
    BoundedCompactSupport (uncurry fun x y ↦ f x * g y) (μ.prod ν) where
…
```
Mentions: MeasureTheory.BoundedCompactSupport, g
theorem MeasureTheory.BoundedCompactSupport.indicator_of_isCompact_closure line 388 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, R1Space, MeasureTheory.MemLp, Top.top, ENNReal, Set, IsCompact, closure, MeasurableSet, MeasureTheory.BoundedCompactSupport, Set.indicator
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.indicator, HasCompactSupport.intro, Not, Membership.mem, of_eq_true, Eq, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, Set.indicator_of_notMem, False, eq_false, notMem_of_notMem_closure, not_false_eq_true, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.indicator line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, MeasureTheory.BoundedCompactSupport, Set, MeasurableSet, Set.indicator
Proof uses: MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.MemLp.indicator, Top.top, ENNReal, MeasureTheory.BoundedCompactSupport.memLp_top, HasCompactSupport.mono, MeasureTheory.BoundedCompactSupport.hasCompactSupport, of_eq_true, LE.le, Function.support, Eq.trans, Inter.inter, True, congrFun', congrArg, Set.support_indicator
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.BoundedCompactSupport.isBoundedTSupport line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENorm, Zero, MeasureTheory.BoundedCompactSupport, Bornology.IsBounded, tsupport
Proof uses: IsCompact.isBounded, MeasureTheory.BoundedCompactSupport.hasCompactSupport
7 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.BoundedCompactSupport.isBoundedSupport line 454 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENorm, Zero, MeasureTheory.BoundedCompactSupport, Bornology.IsBounded, Function.support
Proof uses: Bornology.IsBounded.subset, tsupport, MeasureTheory.BoundedCompactSupport.isBoundedTSupport, subset_tsupport
8 instances, coercions and auxiliary constants left out.
lemma BoundedCompactSupport.mul_bdd_right'' line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MetricSpace, TopologicalSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, Continuous, MeasureTheory.Measure.QuasiMeasurePreserving, MeasureTheory.AEStronglyMeasurable, Set, IsCompact, Inter.inter, Set.preimage, tsupport, Bornology.IsBounded, Set.image, HMul.hMul
Proof uses: MeasureTheory.BoundedCompactSupport.mk, Filter.Eventually, LE.le, Real, Norm.norm, ENNReal.toReal, MeasureTheory.eLpNorm, Top.top, ENNReal, MeasureTheory.ae, MeasureTheory.MemLp.ae_norm_le, MeasureTheory.BoundedCompactSupport.memLp_top, Membership.mem, Exists, MeasureTheory.MemLp, Iff.mp, isBounded_iff_forall_norm_le, IsCompact.isBounded, MeasureTheory.BoundedCompactSupport.hasCompactSupport, MeasureTheory.memLp_top_of_bound and 56 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma BoundedCompactSupport.mul_bdd_left' line 505 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MetricSpace, TopologicalSpace, MeasureTheory.Measure, RCLike, MeasureTheory.BoundedCompactSupport, Continuous, MeasureTheory.Measure.QuasiMeasurePreserving, MeasureTheory.AEStronglyMeasurable, Set, IsCompact, Inter.inter, Set.preimage, tsupport, Bornology.IsBounded, Set.image, HMul.hMul
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, autoParam, funext, mul_comm, BoundedCompactSupport.mul_bdd_right''
61 instances, coercions and auxiliary constants left out.

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