`Carleson/DoublingMeasure.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

80 declarations, 0 contain sorry, 0 declared as axioms

Basic definitions and lemmas

This file contains definitions from Section 2 of the blueprint and used throughout the proof of metric Carleson, as well as results about structures defined in sections 1 and 2 (DoublingMeasure KernelProofData, IsCancellative, FunctionDistances, ...). The constants D, κ, Z from the blueprint are introduce here, and useful inequalities are provided for them (as well as for the constants a and tau).

Imports (3)

Imported by 3 files

lemma seven_le_c line 25 source
standard axioms: propext what this means
Statement uses: LE.le, Nat, OfNat.ofNat, 𝕔
Proof uses: of_eq_true, Eq.trans, True, congrArg, 𝕔_def, eq_true_of_decide, Eq.refl, Bool, Bool.true
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma c_le_100 line 27 source
standard axioms: propext what this means
Statement uses: LE.le, Nat, 𝕔, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, 𝕔_def
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def defaultD The constant D from (2.0.1) line 39 source
Source documentation
The constant D from (2.0.1).

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔
7 instances, coercions and auxiliary constants left out.
```
@[simp] def defaultD (a : ℕ) : ℕ := 2 ^ (𝕔 * a ^ 2)
```
def nnD D as an element of ℝ≥0 line 42 source
Source documentation
D as an element of ℝ≥0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: Subtype.mk, Real, LE.le, OfNat.ofNat, defaultD
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def nnD (a : ℕ) : ℝ≥0 := ⟨defaultD a, by simp⟩
```
Mentions: defaultD
def defaultκ The constant κ from (2.0.2) line 45 source
Source documentation
The constant κ from (2.0.2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, Neg.neg
10 instances, coercions and auxiliary constants left out.
```
def defaultκ (a : ℕ) : ℝ := 2 ^ (-10 * (a : ℝ))
```
def defaultZ The constant Z from (2.0.3) line 48 source
Source documentation
The constant Z from (2.0.3).

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul
7 instances, coercions and auxiliary constants left out.
```
@[simp] def defaultZ (a : ℕ) : ℕ := 2 ^ (12 * a)
…
```
lemma defaultD_pos line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, defaultD
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, 𝕔, id, Eq, congrArg, defaultD.eq_1, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma realD_pos line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, defaultD
Proof uses: cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, defaultD_pos
32 instances, coercions and auxiliary constants left out.
lemma realD_nonneg line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, defaultD
Proof uses: le_of_lt, realD_pos
10 instances, coercions and auxiliary constants left out.
lemma one_le_realD line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, defaultD
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, 𝕔, id, Eq, congrArg, defaultD.eq_1, Nat.cast_pow, Nat.cast_ofNat, Eq.symm, pow_zero, pow_le_pow_right₀, one_le_two
44 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma defaultD_pow_pos line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, Real, OfNat.ofNat, HPow.hPow, defaultD
Proof uses: realD_pos, zpow_pos
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma mul_defaultD_pow_pos line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Int, HMul.hMul, HPow.hPow, defaultD
Proof uses: mul_pos, defaultD_pow_pos
26 instances, coercions and auxiliary constants left out.
lemma hundred_lt_D used in 7.5.6 (limited_scale_impact) line 77 source
Source comment
used in 7.5.6 (`limited_scale_impact`)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, OfNat.ofNat, defaultD
Proof uses: HPow.hPow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Eq, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit1, Bool, Bool.false, LT.lt.trans_le, LE.le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, Neg.neg and 79 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma hundred_lt_D : 100 < defaultD a := by
…
```
Mentions: defaultD
lemma hundred_lt_realD used in 7.5.6 (limited_scale_impact) line 87 source
Source comment
used in 7.5.6 (`limited_scale_impact`)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, Real, OfNat.ofNat, defaultD
Proof uses: cast, Eq.symm, hundred_lt_D
28 instances, coercions and auxiliary constants left out.
```
lemma hundred_lt_realD : (100 : ℝ) < defaultD a := mod_cast hundred_lt_D X
```
Mentions: defaultD, hundred_lt_D
lemma twentyfive_le_realD used in 4.1.7 (small_boundary) line 90 source
Source comment
used in 4.1.7 (`small_boundary`)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LE.le, Real, OfNat.ofNat, defaultD
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 47 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma twentyfive_le_realD : (25 : ℝ) ≤ defaultD a := by linarith [hundred_lt_realD X]
```
Mentions: defaultD, hundred_lt_realD
lemma eight_le_realD used in 4.1.3 (I3_prop_3_1) line 93 source
Source comment
used in 4.1.3 (`I3_prop_3_1`)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LE.le, Real, OfNat.ofNat, defaultD
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 49 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma eight_le_realD : (8 : ℝ) ≤ defaultD a := by linarith [twentyfive_le_realD X]
```
Mentions: defaultD, twentyfive_le_realD
lemma five_le_realD used in 4.1.6 (transitive_boundary) line 96 source
Source comment
used in 4.1.6 (`transitive_boundary`)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LE.le, Real, OfNat.ofNat, defaultD
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 49 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma five_le_realD : (5 : ℝ) ≤ defaultD a := by linarith [twentyfive_le_realD X]
```
Mentions: defaultD, twentyfive_le_realD
lemma four_le_realD used in various places in Carleson.TileExistence line 99 source
Source comment
used in various places in `Carleson.TileExistence`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LE.le, Real, OfNat.ofNat, defaultD
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 49 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma four_le_realD : (4 : ℝ) ≤ defaultD a := by linarith [twentyfive_le_realD X]
```
Mentions: defaultD, twentyfive_le_realD
lemma one_lt_realD line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, Real, OfNat.ofNat, defaultD
Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 47 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma a_pos line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, OfNat.ofNat
Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 44 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma cast_a_pos line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, Real, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_zero, a_pos
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma τ_pos line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, Real, OfNat.ofNat, defaultτ
Proof uses: Iff.mpr, Inv.inv, inv_pos, cast_a_pos
29 instances, coercions and auxiliary constants left out.
lemma τ_nonneg line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LE.le, Real, OfNat.ofNat, defaultτ
Proof uses: LT.lt.le, τ_pos
6 instances, coercions and auxiliary constants left out.
lemma τ_le_one line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LE.le, Real, defaultτ, OfNat.ofNat
Proof uses: Eq.mpr, Inv.inv, id, Eq, congrArg, defaultτ.eq_1, Or, propext, inv_le_one_iff₀, Or.inr, Eq.trans, congrFun', Eq.symm, Nat.cast_one, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd and 54 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def nnτ τ as an element of ℝ≥0 line 115 source
Source documentation
τ as an element of ℝ≥0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, NNReal
Proof uses: Subtype.mk, Real, LE.le, OfNat.ofNat, defaultτ, τ_nonneg
3 instances, coercions and auxiliary constants left out.
```
def nnτ : ℝ≥0 := ⟨defaultτ a, τ_nonneg X⟩
```
Mentions: defaultτ, τ_nonneg
lemma nnτ_pos line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, LT.lt, NNReal, OfNat.ofNat, nnτ
Proof uses: τ_pos
5 instances, coercions and auxiliary constants left out.
lemma nnτ_def line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, Complex, KernelProofData, Eq, NNReal, nnτ, Real.toNNReal, defaultτ
Proof uses: Eq.symm, NNReal.mk, τ_nonneg, Real.toNNReal_of_nonneg
lemma κ_nonneg line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, defaultκ
Proof uses: Real.rpow_nonneg, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, HMul.hMul, Neg.neg
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma κ_le_one line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, defaultκ, OfNat.ofNat
Proof uses: Real.rpow_le_one_of_one_le_of_nonpos, HMul.hMul, Neg.neg, one_le_two, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 47 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 159) line 159 source
instance MeasureTheory.(instance at line 169) line 169 source
def MeasureTheory.DoublingMeasure.mono Monotonicity of doubling measure metric spaces in A line 173 source
Source documentation
Monotonicity of doubling measure metric spaces in A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, LE.le
Proof uses: MeasureTheory.Measure.IsDoubling, MeasureTheory.MeasureSpace.volume, MeasureTheory.DoublingMeasure.mk
14 instances, coercions and auxiliary constants left out.
```
def DoublingMeasure.mono {A'} (h : A ≤ A') : DoublingMeasure X A' where
…
```
Mentions: A, MeasureTheory.DoublingMeasure
instance MeasureTheory.InnerProductSpace.DoublingMeasure line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MeasurableSpace, BorelSpace, FiniteDimensional, MeasureTheory.DoublingMeasure, HPow.hPow, NNReal, Nat, OfNat.ofNat, Module.finrank
Proof uses: MeasureTheory.DoublingMeasure.mk
54 instances, coercions and auxiliary constants left out.
lemma fact_isCompact_ball line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Fact, Bornology.IsBounded, Metric.ball
Proof uses: Fact.mk, Metric.isBounded_ball
2 instances, coercions and auxiliary constants left out.
instance (instance at line 193) line 193 source
def toWithFunctionDistance line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, PseudoMetricSpace, Real, FunctionDistances, Equiv, FunctionDistances.Θ, WithFunctionDistance
Proof uses: Equiv.refl
8 instances, coercions and auxiliary constants left out.
instance nonempty_Space line 204 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, RCLike, PseudoMetricSpace, CompatibleFunctions, Nonempty
Proof uses: FunctionDistances.Θ, Eq, ContinuousMap, FunctionDistances.coeΘ, OfNat.ofNat, Exists, CompatibleFunctions.eq_zero, Nonempty.intro
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance (instance at line 208) line 208 source
lemma le_localOscillation line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, RCLike, PseudoMetricSpace, CompatibleFunctions, Real, FunctionDistances.Θ, Membership.mem, Set, Metric.ball, LE.le, Norm.norm, HAdd.hAdd, HSub.hSub, ContinuousMap, FunctionDistances.coeΘ, ENNReal.toReal, localOscillation
Proof uses: Eq.mpr, ENNReal.ofReal, id, Eq, congrArg, Eq.symm, ENNReal.toReal_ofReal, norm_nonneg, Prod, ENNReal, iSup, SProd.sprod, Prod.fst, Prod.snd, ENNReal.toReal_mono, LT.lt.ne, Top.top, lt_of_le_of_lt, Dist.dist, WithFunctionDistance and 7 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma oscillation_le_cdist line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, RCLike, PseudoMetricSpace, CompatibleFunctions, Real, FunctionDistances.Θ, Membership.mem, Set, Metric.ball, LE.le, Norm.norm, HAdd.hAdd, HSub.hSub, ContinuousMap, FunctionDistances.coeΘ, Dist.dist, WithFunctionDistance
Proof uses: le_trans, ENNReal.toReal, localOscillation, le_localOscillation, Eq.mpr, ENNReal.ofReal, id, Eq, congrArg, Eq.symm, ENNReal.toReal_ofReal, dist_nonneg, ENNReal.toReal_mono, ENNReal.ofReal_ne_top, CompatibleFunctions.localOscillation_le_cdist
61 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma dist_congr line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, PseudoMetricSpace, FunctionDistances, Real, FunctionDistances.Θ, Eq, Dist.dist, WithFunctionDistance
Proof uses: eq_of_heq, Dist, HEq, HEq.refl, Eq.rec, Eq.refl, heq_of_eq
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def cancelPt The point o in the blueprint line 235 source
Source documentation
The point o in the blueprint

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, RCLike, PseudoMetricSpace, CompatibleFunctions
Proof uses: Exists.choose, FunctionDistances.Θ, Eq, ContinuousMap, FunctionDistances.coeΘ, OfNat.ofNat, CompatibleFunctions.eq_zero
18 instances, coercions and auxiliary constants left out.
```
def cancelPt [CompatibleFunctions 𝕜 X A] : X :=
…
```
Mentions: CompatibleFunctions, A
lemma cancelPt_eq_zero line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, RCLike, PseudoMetricSpace, CompatibleFunctions, FunctionDistances.Θ, Eq, cancelPt, OfNat.ofNat
Proof uses: Exists.choose_spec, ContinuousMap, FunctionDistances.coeΘ, CompatibleFunctions.eq_zero
32 instances, coercions and auxiliary constants left out.
lemma enorm_integral_exp_le line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, CompatibleFunctions, Real, IsCancellative, Complex, LE.le, Set, Function.support, Metric.ball, FunctionDistances.Θ, ENNReal, ENorm.enorm, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Complex.exp, Complex.I and 9 more
Proof uses: LT.lt, Or, le_or_gt, of_eq_true, Eq.trans, True, congr, congrArg, funext, congrFun', Eq.mp, Eq, EmptyCollection.emptyCollection, Iff.mpr, Metric.ball_eq_empty, MulZeroClass.mul_zero, MeasureTheory.integral_zero, enorm_zero, Ne, eq_or_ne and 23 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma isCancellative_of_norm_integral_exp_le Constructor of IsCancellative in terms of real norms instead of extended reals line 265 source
Source documentation
Constructor of IsCancellative in terms of real norms instead of extended reals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, Real, CompatibleFunctions, Complex, LT.lt, OfNat.ofNat, Ne, ENNReal, iLipENorm, Top.top, LE.le, Set, Function.support, Metric.ball, FunctionDistances.Θ, Norm.norm, MeasureTheory.integral and 14 more
Proof uses: IsCancellative.mk, Eq.mpr, ENorm.enorm, MeasureTheory.Measure, EDist.edist, ENNReal.ofReal, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, id, congrArg, ofReal_norm, ENorm, Eq.rec, MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero, Not and 40 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma isCancellative_of_norm_integral_exp_le (τ : ℝ) [CompatibleFunctions ℝ X A]
    (h : ∀ {x : X} {r : ℝ} {φ : X → ℂ} (_hr : 0 < r) (_h1 : iLipENorm φ x r ≠ ∞)
    (_h2 : support φ ⊆ ball x r) {f g : Θ X},
      ‖∫ x in ball x r, exp (I * (f x - g x)) * φ x‖ ≤
      A * volume.real (ball x r) * iLipNNNorm φ x r * (1 + dist_{x, r} f g) ^ (-τ)) :
    IsCancellative X τ := by
…
```
Mentions: CompatibleFunctions, A, iLipENorm, g, iLipNNNorm, IsCancellative
def vol The "volume function" V line 295 source
Source documentation
The "volume function" V. We will need to assume IsFiniteMeasureOnCompacts and ProperSpace to actually know that this volume is finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, ENNReal
Proof uses: MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Metric.ball, Dist.dist
4 instances, coercions and auxiliary constants left out.
```
def vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ≥0∞ :=
…
```
lemma measurable_vol line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, SecondCountableTopology, MeasureTheory.MeasureSpace, OpensMeasurableSpace, MeasureTheory.SFinite, MeasureTheory.MeasureSpace.volume, Measurable, Prod, ENNReal, Function.uncurry, vol
Proof uses: Real, Prod.mk, Dist.dist, MeasureTheory.Measure, Set, Metric.ball, Measurable.comp, MeasureTheory.measurable_measure_ball, Measurable.prodMk, Prod.fst, Prod.snd, Measurable.fst, measurable_id', Measurable.dist, Measurable.snd
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma measurable_vol₁ line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, SecondCountableTopology, MeasureTheory.MeasureSpace, OpensMeasurableSpace, MeasureTheory.SFinite, MeasureTheory.MeasureSpace.volume, Measurable, ENNReal, vol
Proof uses: id, Measurable.comp, Prod, Function.uncurry, Prod.mk, measurable_vol, Measurable.prodMk, measurable_id', measurable_const
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Real.vol_def line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, Eq, Real, Real.vol, ENNReal.toReal, vol
Proof uses: rfl
lemma ofReal_vol line 318 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.MeasureSpace.volume, Eq, ENNReal, ENNReal.ofReal, Real.vol, vol
Proof uses: id, Eq.mpr, ENNReal.toReal, Ne, Top.top, MeasureTheory.measure_ball_ne_top, Dist.dist
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma le_upperRadius line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, FunctionDistances, Real, FunctionDistances.Θ, LT.lt, Dist.dist, WithFunctionDistance, OfNat.ofNat, LE.le, ENNReal, ENNReal.ofReal, upperRadius
Proof uses: le_iSup₂
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma carlesonOperatorIntegrand_const_smul line 328 source
lemma linearizedCarlesonOperator_const_smul line 337 source
lemma carlesonOperator_const_smul line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, FunctionDistances, Real, Complex, Eq, ENNReal, carlesonOperator, HSMul.hSMul, ENorm.enorm
Proof uses: id, Eq.mpr, iSup, FunctionDistances.Θ, linearizedCarlesonOperator, congrFun', congrArg, funext, congrFun, Eq.refl
65 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma nontangentialOperator_const_smul line 350 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, Complex, Eq, ENNReal, nontangentialOperator, HSMul.hSMul, ENorm.enorm
Proof uses: id, Eq.mpr, iSup, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Metric.ball, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, congrFun', congrArg, funext, iSup_congr_Prop, Iff.of_eq, Eq.refl and 4 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma carlesonOperatorIntegrand_const_smul' line 356 source
lemma linearizedCarlesonOperator_const_smul' line 365 source
lemma carlesonOperator_const_smul' line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, FunctionDistances, Real, Complex, Eq, ENNReal, carlesonOperator, HSMul.hSMul, ENorm.enorm
Proof uses: id, Eq.mpr, iSup, FunctionDistances.Θ, linearizedCarlesonOperator, congrFun', congrArg, funext, congrFun, Eq.refl
65 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma C_K_pos line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, NNReal, OfNat.ofNat, C_K
Proof uses: NNReal.rpow_pos, HPow.hPow, Nat, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma C_K_pos_real line 388 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, C_K
Proof uses: C_K_pos
4 instances, coercions and auxiliary constants left out.
lemma isOneSidedKernel_const_smul line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, Nat, Complex, IsOneSidedKernel, Real, LE.le, abs, OfNat.ofNat, HSMul.hSMul
Proof uses: IsOneSidedKernel.mk, Measurable.const_smul, Prod, Function.uncurry, IsOneSidedKernel.measurable_K, Eq.mpr, Norm.norm, HDiv.hDiv, C_K, Real.vol, HMul.hMul, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans and 25 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.stronglyMeasurable_K line 405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, IsOneSidedKernel, MeasureTheory.StronglyMeasurable, Prod, Function.uncurry
Proof uses: Measurable.stronglyMeasurable, IsOneSidedKernel.measurable_K
27 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.aestronglyMeasurable_K line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, IsOneSidedKernel, MeasureTheory.AEStronglyMeasurable, Prod, Function.uncurry, MeasureTheory.MeasureSpace.volume
Proof uses: Measurable.aestronglyMeasurable, IsOneSidedKernel.measurable_K
29 instances, coercions and auxiliary constants left out.
lemma measurable_K_left line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, IsOneSidedKernel, Measurable
Proof uses: Measurable.of_uncurry_right, IsOneSidedKernel.measurable_K
4 instances, coercions and auxiliary constants left out.
lemma measurable_K_right line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, IsOneSidedKernel, Measurable
Proof uses: Measurable.of_uncurry_left, IsOneSidedKernel.measurable_K
4 instances, coercions and auxiliary constants left out.
lemma enorm_K_le_vol_inv line 419 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.MeasureSpace.volume, IsOneSidedKernel, LE.le, ENNReal, ENorm.enorm, HDiv.hDiv, C_K, Real, vol
Proof uses: Eq.mpr, ENNReal.ofReal, Norm.norm, id, Eq, congrArg, Eq.symm, ofReal_norm, Real.vol, ofReal_vol, ENNReal.ofReal_coe_nnreal, le_trans, ENNReal.ofReal_le_ofReal, IsOneSidedKernel.norm_K_le_vol_inv, ENNReal.ofReal_div_le, MeasureTheory.measureReal_nonneg, Metric.ball, Dist.dist
48 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma enorm_K_le_ball_complement line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.MeasureSpace.volume, IsOneSidedKernel, Real, Membership.mem, Set, Compl.compl, Metric.ball, LE.le, ENNReal, ENorm.enorm, HDiv.hDiv, C_K, MeasureTheory.Measure
Proof uses: le_trans, vol, enorm_K_le_vol_inv, ENNReal.div_le_div_left, Dist.dist, MeasureTheory.measure_mono, Metric.ball_subset_ball, Eq.mp, Eq.trans, Not, LT.lt, congrArg, congrFun', dist_comm
58 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma enorm_K_le_ball_complement' line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.IsOpenPosMeasure, IsOneSidedKernel, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Compl.compl, Metric.ball, LE.le, ENNReal, ENorm.enorm, ENNReal.toNNReal and 3 more
Proof uses: Eq.mpr, id, Eq, congrArg, ENNReal.coe_toNNReal, Ne, Top.top, Not, Ne.eq_1, Or, And, propext, ENNReal.div_eq_top, Eq.trans, congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, of_eq_true, True and 10 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma enorm_K_sub_le line 443 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.MeasureSpace.volume, IsOneSidedKernel, LE.le, Real, HMul.hMul, OfNat.ofNat, Dist.dist, ENNReal, ENorm.enorm, HSub.hSub, HPow.hPow, HDiv.hDiv, EDist.edist, Inv.inv and 2 more
Proof uses: Eq.mpr, ENNReal.ofReal, Norm.norm, id, Eq, congrFun', congrArg, Real.vol, congr, edist_dist, Trans.trans, ENNReal.ofReal_le_ofReal, IsOneSidedKernel.norm_K_sub_le, ENNReal.ofReal_mul', div_nonneg, NNReal.zero_le_coe, MeasureTheory.measureReal_nonneg, Metric.ball, mul_le_mul', Eq.symm and 6 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma integrableOn_K_mul line 459 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.MeasureSpace.volume, MeasureTheory.IsFiniteMeasureOnCompacts, ProperSpace, IsOneSidedKernel, Set, MeasureTheory.IntegrableOn, Real, LT.lt, OfNat.ofNat, LE.le, Compl.compl, Metric.ball, HMul.hMul
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.Measure.restrict, MeasureTheory.HasFiniteIntegral, AEMeasurable.aestronglyMeasurable, AEMeasurable.mul, AEMeasurable.restrict, Measurable.aemeasurable, measurable_K_right, MeasureTheory.Integrable.aemeasurable, Iff.mpr, ENNReal, MeasureTheory.lintegral, ENorm.enorm, Top.top, MeasureTheory.hasFiniteIntegral_def, Trans.trans, HDiv.hDiv, C_K, MeasureTheory.Measure and 24 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma integrableOn_K_Icc line 472 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, MeasureTheory.MeasureSpace, MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.MeasureSpace.volume, MeasureTheory.IsFiniteMeasureOnCompacts, ProperSpace, IsOneSidedKernel, Real, GT.gt, OfNat.ofNat, MeasureTheory.IntegrableOn, Set.ofPred, Membership.mem, Set, Set.Icc, Dist.dist
Proof uses: Eq.mpr, HMul.hMul, id, Eq, congrArg, Eq.symm, mul_one, integrableOn_K_mul, LE.le, Metric.closedBall, Set.Annulus.cc_subset_closedBall, MeasureTheory.integrableOn_const, Complex.mk, LT.lt.ne, ENNReal, MeasureTheory.Measure, Top.top, LE.le.trans_lt, MeasureTheory.measure_mono, MeasureTheory.measure_closedBall_lt_top and 12 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma le_cdist_iterate line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, CompatibleFunctions, Real, defaultA, LE.le, OfNat.ofNat, FunctionDistances.Θ, HMul.hMul, HPow.hPow, Dist.dist, WithFunctionDistance
Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, pow_zero, one_mul, Lean.Meta.Rfl.rel_of_eq_and_refl, eq_of_heq, Dist, HEq, Eq.refl, HEq.refl, Eq.symm, RCLike, FunctionDistances, of_eq_true, Eq.trans, True, congrFun' and 32 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma cdist_le_iterate line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, CompatibleFunctions, Real, defaultA, LT.lt, OfNat.ofNat, FunctionDistances.Θ, LE.le, Dist.dist, WithFunctionDistance, HMul.hMul, HPow.hPow
Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, congrFun', pow_zero, one_mul, Lean.Meta.Rfl.rel_of_eq_and_refl, eq_of_heq, Dist, HEq, Eq.refl, HEq.refl, Eq.symm, RCLike, FunctionDistances, of_eq_true, Eq.trans, True and 49 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma cdist_le_mul_cdist line 521 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, CompatibleFunctions, Real, defaultA, LT.lt, OfNat.ofNat, FunctionDistances.Θ, LE.le, Dist.dist, WithFunctionDistance, HMul.hMul, As, NNReal, HDiv.hDiv, HAdd.hAdd
Proof uses: Trans.trans, HPow.hPow, Nat.ceil, Real.logb, CompatibleFunctions.cdist_mono, Metric.ball_subset_ball', Eq, Eq.symm, div_mul_cancel₀, LT.lt.ne', mul_le_mul_of_nonneg_right, Real.le_pow_natCeil_logb, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, div_pos and 4 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ballsCoverBalls_iterate_nat line 535 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, CompatibleFunctions, Real, defaultA, BallsCoverBalls, WithFunctionDistance, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: AllBallsCoverBalls.pow, CompatibleFunctions.allBallsCoverBalls
23 instances, coercions and auxiliary constants left out.
lemma ballsCoverBalls_iterate line 539 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, CompatibleFunctions, Real, defaultA, LT.lt, OfNat.ofNat, BallsCoverBalls, WithFunctionDistance, HPow.hPow, Nat.ceil, Real.logb, HDiv.hDiv
Proof uses: AllBallsCoverBalls.ballsCoverBalls, CompatibleFunctions.allBallsCoverBalls, one_lt_two
59 instances, coercions and auxiliary constants left out.
lemma measurable_Q₂ line 550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Measurable, Prod, Prod.fst, Prod.snd
Proof uses: Set, MeasurableSet, Eq, Set.preimage, Set.iUnion, Membership.mem, Finset, MeasureTheory.SimpleFunc.range, SProd.sprod, Singleton.singleton, Set.ext, Iff, Eq.mpr, Prod.mk, Exists, And, id, congr, congrArg, Eq.trans and 17 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma stronglyMeasurable_Q₂ line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, MeasureTheory.StronglyMeasurable, Prod, Prod.fst, Prod.snd
Proof uses: Measurable.stronglyMeasurable, measurable_Q₂
50 instances, coercions and auxiliary constants left out.
lemma aestronglyMeasurable_Q₂ line 563 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, MeasureTheory.AEStronglyMeasurable, Prod, Prod.fst, Prod.snd, MeasureTheory.MeasureSpace.volume
Proof uses: Measurable.aestronglyMeasurable, measurable_Q₂
52 instances, coercions and auxiliary constants left out.
lemma measurable_Q₁ line 567 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Measurable
Proof uses: Eq, rfl, Eq.rec, Measurable.of_uncurry_left, measurable_Q₂
40 instances, coercions and auxiliary constants left out.