Bump mathlib to latest master and fix compatibility

[zixiaowang17]

Summary

• bump mathlib from v4.33.1 to the latest master commit dd56d02cb7a58fa066c4a2c7fddec3cbb59ae8df
• update Lean from v4.33.1 to v4.35.0-rc3
• simplify Contiguous2 and Contiguous3 to use the new ProbabilityMeasure.map API, following @CoolRmal's review comment
• migrate proof bodies for the current EReal, MemLp, and Radon-Nikodym APIs without changing theorem statements
• preserve the intentional PosPart compatibility simp lemmas with targeted nolint simpNF annotations

Verification

• lake build
• lake lint
• lake exe mk_all --check

All three checks pass locally against the pinned mathlib commit above. This resolves the compatibility failures reported in #48.

[zixiaowang17]

hey @CoolRmal , could you please take a look at this line of definition of your contiguity files??

[CoolRmal]

def Contiguous2 (l : Filter α) (P Q : ∀ a, ProbabilityMeasure (Ω a)) : Prop :=
  ∀ (L : ProbabilityMeasure ℝ≥0∞) ⦃h : Filter α⦄, h ≤ l → h.NeBot →
    Tendsto (fun a ↦ (Q a).map ((P a : Measure (Ω a)).rnDeriv (Q a))) h (𝓝 L) →
      L {0} = 0

def Contiguous3 (l : Filter α) (P Q : ∀ a, ProbabilityMeasure (Ω a)) : Prop :=
  ∀ (V : ProbabilityMeasure ℝ≥0∞) ⦃h : Filter α⦄, h ≤ l → h.NeBot →
    Tendsto (fun a ↦ (P a).map ((Q a : Measure (Ω a)).rnDeriv (P a))) h (𝓝 V) →
      ∫⁻ ω, ω ∂V = 1

With the newer mathlib API, a proof that the rnDeriv is measurable is not needed.

[zixiaowang17]

@CoolRmal Thanks! pushed another commit and other related fix