Buffon's Needle general lemmas

Stream: mathlib4

[Enrico Borba]

As part of getting my formalization of Buffon's needle into the mathlib archive, I wanted to get opinions on what I think is the only lemma general enough to be a candidate for addition into mathlib:

lemma set_integral_toReal_ofReal_nonneg_ae [MeasureSpace α] {s : Set α} {f : α → ℝ}
    (hs : MeasurableSet s) (hf : ∀ᵐ x : α, x ∈ s → f x ≥ 0) :
    ∫ (x : α) in s, ENNReal.toReal (ENNReal.ofReal (f x)) =
    ∫ (x : α) in s, f x := by

  have toReal_ofReal_eq_iff (r : ℝ) : r = ENNReal.toReal (ENNReal.ofReal r) ↔ r ≥ 0 := by
    apply Iff.intro
    · intro hr; rw [hr]; exact ENNReal.toReal_nonneg
    · intro hr; exact (ENNReal.toReal_ofReal hr).symm

  have : ∀ᵐ x : α, x ∈ s → f x = ENNReal.toReal (ENNReal.ofReal (f x)) := by
    simp_rw [toReal_ofReal_eq_iff]
    exact hf

  rw [MeasureTheory.set_integral_congr_ae hs this]

Thoughts on 1) whether it should be added at all 2) naming?

[Johan Commelin]

The subclaim

lemma toReal_ofReal_eq_iff (r : ℝ) : ENNReal.toReal (ENNReal.ofReal r) = r ↔ r ≥ 0 := by
    apply Iff.intro
    · intro hr; rw [hr]; exact ENNReal.toReal_nonneg
    · intro hr; exact (ENNReal.toReal_ofReal hr).symm

seems like a good addition, if it isn't there yet.

[Johan Commelin]

(I swapped the two sides of the = in the statement, but didn't adjust the proof.)

[Enrico Borba]

Yeah it's in that order b/c of what set_integral_congr_ae expects. That's a good suggestion for addition.

[Enrico Borba]

Ok, I'll make a PR for that one at least :)

[Riccardo Brasca]

The first one looks to me a little too specific, and the proof is very short, I don't think it is worth having it. Unless of course you use it very often.

[Johan Commelin]

@Enrico Borba Please let me know your github username. Then I'll give you the required write access to mathlib non-master branches.

[Enrico Borba]

I think I have permission? I made a small PR a little earlier, it's enricozb if could confirm that though :)

[Johan Commelin]

Ok, that's good

[Enrico Borba]

Whoops look like it already exists haha (docs#ENNReal.toReal_ofReal_eq_iff). I guess I don't have anything to add then. @Johan Commelin with respect to adding my formalization to the archive, is there anything I need to do other than 1) styling, 2) ensure it builds with the latest mathlib?

[Johan Commelin]

That's about it. Just create a PR that adds Buffon.lean to the Archive/ folder.

[Enrico Borba]

Sweet

[Ruben Van de Velde]

You might add a module docstring with a short overview of the statement and the proof

[Johan Commelin]

Yeah, I was about to say that. As part of the "1) styling" please add a bunch of docs and explanations.

[Enrico Borba]

Ah good idea, I'll look at some of the other Archive ones for inspiration

[Enrico Borba]

Do I need to reference my file under Archive/Wiedijk100Theorems to make sure it's checked?

[Johan Commelin]

It doesn't influence checking. But you should still fill in the entry there.

[Ruben Van de Velde]

It needs to be in Archive.lean, though

[Ruben Van de Velde]

And ./docs/100.yaml

[Ruben Van de Velde]

(Not for checking, but for the website)

[Enrico Borba]

Ruben Van de Velde said:

It needs to be in Archive.lean, though

Ah that's what I was looking for, thanks