Fill scalar multiplication of finitely additive measures

[Chessing234]

Fill finite additivity of scalar multiples of finitely additive measures. Use nonnegativity on measurable sets to apply EReal.left_distrib_of_nonneg; unrestricted extended-real distributivity is unavailable. The scalar nonnegativity proof also uses the explicit ENNReal coercion lemma.

Validation: an isolated Lean check with the actual structure and scalar-multiplication declaration fails for the previous proof (missing CanonicallyOrderedAdd EReal and LeftDistribClass EReal) and passes for the corrected proof.

Full chapter validation is blocked by existing errors in Sections 1.4.1–1.4.3. PR #711 repairs Sections 1.4.1 and 1.4.2, but Section 1.4.3 still fails. The default root currently omits Section 1.4.3, so the ordinary CI check does not validate this change. Keeping this draft until the shared chapter builds.

[teorth]

Thanks — the content here is good, and I've merged 29 of the sibling PRs from this batch (#686–#718). This one now needs a rebase onto main before it can go in.

The conflict is purely positional, not substantive: a sibling PR filled other fields of the same structure literal, and git can't line up the context. Concretely, one side of the conflict has the fields that sibling filled (with your field still sorry), and the other side has your field filled (with theirs still sorry). The resolution is just the union — take whichever side has the real proof for each field, discarding the sorry version.

I resolved all four of the conflicting PRs that way locally and ran a full lake build: 8310 jobs, no errors. So this is mechanical, and nothing about your proof needs to change.

One suggestion for future batches, since this cost four PRs a round-trip: when several PRs fill different fields of the same structure literal, they will always conflict with each other even though each is individually mergeable against main. Grouping the fields of one structure into a single PR avoids it entirely — and would be easier to review, too.

[Chessing234]

rebased onto main. kept each field that already had a proof, and the one this pr fills.