Lemma 7.1.4 #201
Lemma 7.1.4 #201
Conversation
|
Thanks! This looks good! |
Carleson/ToMathlib/Misc.lean
Outdated
| open Classical in | ||
| theorem setIntegral_biUnion_le_sum_setIntegral {X : Type*} {ι : Type*} [MeasurableSpace X] | ||
| {f : X → ℝ} (s : Finset ι) {S : ι → Set X} {μ : Measure X} | ||
| (meas_f : Measurable f) (f_ae_nonneg : ∀ᵐ (x : X) ∂μ, x ∈ (⋃ i ∈ s, S i) → 0 ≤ f x) |
There was a problem hiding this comment.
Can you prove this without assuming Measurable f? You get a.e.-measurability from the integrability, and that should be enough: the conclusion is invariant under a.e.-equality.
If you remove that assumption, I think you also don't need the primed version?
There was a problem hiding this comment.
Actually, this whole theorem was unnecessary. I forgot that the sets involved are disjoint, and there's already a theorem in Mathlib for handling that case. Would you like me to try to clean it up anyway and leave it here even though it's not being used, so that it can be submitted to Mathlib as a product of the Carleson project? Or should I remove it and submit it on my own?
There was a problem hiding this comment.
Either of these two options are completely fine by me. Feel free to clean it up and leave it here (maybe with a comment currently unused) before upstreaming it or remove it here.
There was a problem hiding this comment.
Done. I also generalized it further so that it only assumes IntegrableOn instead of Integrable.
|
Thanks for the fixes of the blueprint, they all look good to me. I'll edit the proof of 7.2.3 |
I added two theorems in the ToMathlib file. We might also consider generalizing `sum_pow_two_le` (in PointwiseEstimate.lean) and adding it to Mathlib; Mathlib has some results about geometric sums indexed by naturals, but none that I could find about geometric sums indexed by integers. There were a few (as far as I could tell) mistakes in the blueprint, which I fixed: - There were a couple uninteresting typos. - There was some confusion about the constant `C7_1_4 a`: in the statement of the theorem, it's 10 * 2 ^ (105a^3), but at the end of the proof, it's 2 ^ (105a^3). I changed it to 10 * 2 ^ (104a^3). - I don't think that the step originally described in the blueprint as "[u]sing the doubling property (1.0.8), the definition of d_p and Lemma 2.1.2" works as written. The doubling property requires x_1 to be in B_2, which I don't think can be proven in this situation. I used the monotonicity property (1.0.9) to make the balls big enough that this condition holds; this requires more applications of (1.0.8) to compensate, but the extra factors from (1.0.8) eventually get absorbed into the constant, with the same result as originally in the blueprint. - The proof claims that (7.1.1) says that 𝒥 is a partition of X, but (7.1.1) actually says that 𝒥 is a partition of the union of the dyadic cubes; I don't see any assumption that the dyadic cubes cover all of X. I changed the reference accordingly. (I noticed that the same claim about 𝒥 being a partition of X is made in the proof of Lemma 7.2.3, but I didn't edit that part.) - Toward the end, the blueprint says "we have s(L) <= s(p) for all p," but I think that conclusion is only valid assuming L and p are not disjoint. That doesn't cause any problems for the proof, because we have nondisjointness in the relevant case; I edited the blueprint to avoid the stronger claim. --------- Co-authored-by: Floris van Doorn <[email protected]>
I added two theorems in the ToMathlib file. We might also consider generalizing
sum_pow_two_le(in PointwiseEstimate.lean) and adding it to Mathlib; Mathlib has some results about geometric sums indexed by naturals, but none that I could find about geometric sums indexed by integers.There were a few (as far as I could tell) mistakes in the blueprint, which I fixed:
C7_1_4 a: in the statement of the theorem, it's 10 * 2 ^ (105a^3), but at the end of the proof, it's 2 ^ (105a^3). I changed it to 10 * 2 ^ (104a^3).