Conversation
|
@grunweg, why was the |
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
That was a large one - thanks a lot for your help here!
I have a few comments about possible clean-up. All comments inside Carleson are optional.
| congr 1; simp_rw [← mul_assoc] | ||
| rw [← lintegral_biUnion_finset _ (fun _ _ ↦ measurableSet_E)] | ||
| · simp | ||
| · simp only [Finset.mem_filter, Finset.mem_univ, true_and] |
There was a problem hiding this comment.
Is this change needed? Mathlib style is to actually prefer using plain simp when that works: https://leanprover-community.github.io/contribute/style.html#squeezing-simp-calls
This is inside the Carleson directory, so not critical for merging --- but I guess you'd like to know anyway.
There was a problem hiding this comment.
Surprisingly, yes!
simp doesn't work anymore.
Same goes for all similar chages, if I touched it then it was erroring out (didn't touch nonerrory lines to make git diff a bit easier).
https://leanprover-community.github.io/contribute/style.html#squeezing-simp-calls
Thanks, haven't seen it!
| exact ⟨⟨hx.1.1, hx.2⟩, lt_trans hQ one_lt_two⟩ | ||
| simp only [E₂, TileLike.toSet, smul_fst, smul_snd, mem_inter_iff, mem_preimage] | ||
| refine ⟨⟨hx.1.1, hx.2⟩, ?_⟩ | ||
| apply @ball_subset_ball (WithFunctionDistance (𝔠 p) (↑D ^ 𝔰 p / 4)) instPseudoMetricSpaceWithFunctionDistance _ 1 2 (by norm_num) |
There was a problem hiding this comment.
Could gcongr help here? (Otherwise, the WithFunctionDistance details smell like some latent defeq abuse... which could be nice to fix, given infinite time.)
There was a problem hiding this comment.
gcongr doesn't help, but slightly refactored it via other means
| exact ENNReal.le_coe_iff.mp h2r | ||
| exact ENNReal.le_coe_iff.mp h2d | ||
| exact ENNReal.le_coe_iff.mp h2c | ||
| refine le_iSup₂_of_le p hp ?_ |
There was a problem hiding this comment.
Much nicer proof, by the way - thanks!
| · refine le_iSup₂_of_le p (mem_lowerCubes.mpr ⟨p, hp, le_refl _⟩) ?_ | ||
| refine le_iSup_of_le (le_refl _) ?_ | ||
| gcongr | ||
| · simp only [NNReal.coe_ofNat, subset_refl] |
| · rw [dist_comm (α := WithFunctionDistance (𝔠 p) (D ^ 𝔰 p / 4)) _ (𝒬 q)] | ||
| exact (hex q hq).choose_spec.2 | ||
| · rw [dist_comm (α := WithFunctionDistance (𝔠 p) (D ^ 𝔰 p / 4)) _ (𝒬 q')] | ||
| rw [←hfq, hf, hfq'] |
There was a problem hiding this comment.
Can the two rws be combined?
There was a problem hiding this comment.
Yes, and turns out (α := WithFunctionDistance) can be removed now. Changed.
| · refine mem_ae_iff.mpr ?_ | ||
| rw [NNReal.volume_val] | ||
| simp | ||
| rw [ |
There was a problem hiding this comment.
This proof is inside ToMathlib --- so it would be good to understand what's going on. Can you at least some a "TODO" or "adaptation note", pointing to the Lean version bump?
| exact hx | ||
| rw [NNReal.volume_val, this] | ||
| simpa only [Real.volume_Ioo, ENNReal.ofReal_eq_ofNat] using by norm_num | ||
| rw [NNReal.volume_val] |
| simp only [val_eq_coe] | ||
| rw [toReal_Iio_eq_Ico, Real.volume_Ico] | ||
| simp | ||
| change volume (NNReal.toReal '' Set.Iio b) = b |
There was a problem hiding this comment.
Though, can you try to figure out to replace the change by something explicit (in all four places in this file)?
There was a problem hiding this comment.
Can be changed into erw (link). Not more explicit, but good it's shorter?
I would say it was never enabled :-) My best guess is that this project has really two kinds of style, and inside |
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
2 participants
Continues with migration to Lean v4.29 (#545)
TODOs:
integral_smth(integral_conj, etc.) can be further shortened into_ = (starRingEnd ℂ) (∫ y in _, _)set_option backward.isDefEq.respectTransparency falseinstance NNReal.MeasureSpaceCalculations.leancan now be shortened into plainsimp