feat: close the integral tendsto zero sorries in uniformIntegrable_predictableSeqTop (#451)

[raphaelrrcoelho]

closes #451.

fills the two Tendsto.add sorries in uniformIntegrable_predictableSeqTop (the integral tendsto zero step). both summands are discharged by a new private helper tendsto_iSup_setIntegral_tauMesh_zero: for a non-positive a and a level b c → ∞, the supremum over meshes of ∫ a * stoppedValue over {τₙ(b c) < ⊤} tends to 0. it takes the uniform-integrability δ from hd, uses measure_tauMesh_lt_top_le to push every hitting set below δ once c is large, and bounds each term through the L¹ eLpNorm / setIntegral identity. also proves isStoppingTime_tauMeshLift (the lift of τₙ(c) to a 𝓕-stopping time), which was a sorry and is needed to apply hd to the lifted stopping times.

[raphaelrrcoelho]

awaiting-review

[CoolRmal]

May you tell me your AI usage for this PR? I am not against you using it, but I just want to make sure you carefully reviewed every single line of this PR.

[raphaelrrcoelho]

hi @CoolRmal. I directed Claude heavily here, both to translate the standard argument for this (see below) and for making sure it was idiomatic with the patterns in this repo. It wrote the lean code under my direction.

I reviewed the results and they are aligned with the standard way to look at this. It's essentially a lift in the mesh stopping time t_n(c) to a F-stopping time, then show the two sup-over-mesh set-integrals tend to 0. It consumes the existing api rather than trying to re-proving anything.

I've gone through the final diff and can walk through. happy to adjust naming/structure, or to split the isStoppingTime_tauMeshLift into smaller PRs.

[raphaelrrcoelho]

Maybe to share a little, I'm particularly interested in having this lane into the repo because it's usable for my personal project on financial math, which consumes this.

[CoolRmal]

I think tendsto_iSup_setIntegral_tauMesh_zero is a very useful lemma to have. That said, I wonder if the proof could be reorganized a bit. At the moment, it feels somewhat tailored to this particular sorry, and I find it a little hard to see the overall structure of the argument from the code. In particular, the epsilon–delta details seem to obscure the main idea of the proof.

How about this? We basically want to show that

Let's make the following abstraction. You basically have a uniformly integrable collection of random variables indexed by the pair $$(n,c)$$, so naturally we would like to prove a lemma like the following.

lemma UniformIntegrable.eLpNorm_tendsto_zero_of_iSup_measure_tendsto_zero
    {α ι κ Ω E} [MeasurableSpace Ω] {μ : Measure Ω} [NormedAddCommGroup E]
    {X : α → Ω → E} {p : ℝ≥0∞} (hX : UniformIntegrable X p μ)
    {A : κ → ι → Set Ω} {F : κ → ι → α} {l : Filter κ}
    (hA : Tendsto (fun k ↦ ⨆ i, μ (A k i)) l (𝓝 0)) :
    Tendsto (fun k ↦ ⨆ i, eLpNorm ((A k i).indicator (X (F k i))) p μ) l (𝓝 0) := by
  sorry

I imagine this can be a very useful lemma to have in mathlib. I think it is much better if you leave the epsilon delta details inside this lemma, and apply this lemma to prove tendsto_iSup_setIntegral_tauMesh_zero. You probably need an additional assumption on p in UniformIntegrable.eLpNorm_tendsto_zero_of_iSup_measure_tendsto_zero, but I'll let you figure that out.

[raphaelrrcoelho]

I see. It makes sense. I was overly focused on the sorrys

i'll lift the core into UniformIntegrable.eLpNorm_tendsto_zero_of_iSup_measure_tendsto_zero. the delta comes straight from the UnifIntegrable field. The only extra side-conditions i'll need are measurability of the sets and p diff drom inf.

[CoolRmal]

Can you resolve the conversation if you think you have addressed my comments?
Also I think you are not really following the coding style that I pointed out in the comments above in your new proof (you should read this https://leanprover-community.github.io/contribute/style.html if you have more doubts about the coding style). May you try harder on golfing the proof and make it more concise?

[raphaelrrcoelho]

@CoolRmal I converted it to draft again so I can work on your feedback.

I'm going for a rework on tendsto_iSup_setIntegral_tauMesh_zero to be in three steps: a) the |a|·L¹-norm identity; b) the measures shrinking; c) a reducing to the norms vanishing.

Plus I will drop the redundant haves (fold hmesh/hg_int in, remove the intermediate hnorm, etc), and switch to have-binders instead of intro, simpa, etc

[raphaelrrcoelho]

@CoolRmal just FYI, the PR is ready for review.