Measure theory 1.3.2: add nonneg hypotheses from issue #517

[Chessing234]

Summary

• UnsignedMeasurable.aeEqual / .aeLimit concluded unsigned measurability from a.e. data only.
• UnsignedMeasurable.comp_cts allowed a continuous φ that sends some nonnegative values negative.

Root cause

UnsignedMeasurable requires f x ≥ 0 at every point. A.e. equality/limit does not preserve a single negative point (null set). Composition with e.g. φ = (· - 1) can negate values even when f is unsigned measurable.

Fix

Add Unsigned g, Unsigned f, and ∀ x ≥ 0, φ x ≥ 0 respectively.

Test plan

• lake build Analysis/MeasureTheory/Section_1_3_2.lean

Fixes part of #517.