fix(MeasureTheory): Section 1.4 was never in the build; add imports and repair it

[teorth]

The problem

Analysis.lean does not import Section_1_4_1, Section_1_4_2 or Section_1_4_3. Since lake build builds the Analysis target, none of those three files has ever been compiled by lake build or by CI.

They had consequently drifted into a state where all three failed to compile. No CI run could have reported this: every PR touching Section 1.4 got a green check that never looked at the file it changed. (I merged a number of such PRs myself over the last few weeks, on exactly that false signal.)

What this does

Adds the three missing imports — the build goes from 8310 to 8313 jobs — and repairs Section_1_4_3, which was the only one still failing once #711, #694, #700 and #712 had landed. (#711 deserves credit here: it spotted the missing Section_1_4_2 import and fixed the genuinely broken compl_mem fields in 1.4.1.)

The main repair is missing API. FinitelyAdditiveMeasure and CountablyAdditiveMeasure had no @[ext] lemma, so the ext tactic did not apply to them, yet several instance proofs were written as cases …; congr 1; ext A in the hope that it would. Both are one function field plus propositions, so extensionality follows from funext and proof irrelevance:

@[ext] theorem FinitelyAdditiveMeasure.ext … (h : ∀ A, μ.measure A = ν.measure A) : μ = ν

With those registered, the AddCommMonoid and DistribMulAction instance proofs collapse to ext A plus the pointwise fact. Two other fixes:

• FinitelyAdditiveMeasure.restrict — Disjoint.image wants an InjOn and two subset side conditions, and the image of a union needed Set.image_union.
• lebesgue_isCountablyAdditive — Lebesgue_measure.countable_union takes its family implicitly, so the field needs it eta-expanded.

One thing left open, deliberately

smul_add is sorry in both DistribMulAction instances, with a comment, rather than papered over. Pointwise it asks for

c * (μ A + ν A) = c * μ A + c * ν A

for an arbitrary set A. But EReal is distributive only over nonnegative summands (EReal.left_distrib_of_nonneg), and FinitelyAdditiveMeasure.measure_pos constrains the sign of μ A only for B-measurable A. So as the definitions currently stand this field is not provable, and DistribMulAction ENNReal (FinitelyAdditiveMeasure B) cannot be instantiated as written. That is a design question — restrict the measure field to measurable sets, require a global sign condition, or weaken the algebraic structure — rather than something to settle in a repair PR.

Verification

lake build: 8313 jobs, no errors. Net change to sorry count in Section_1_4_3 is +2, both the smul_add fields above; everything else that previously failed to compile now compiles.

Worth considering separately: a CI check that every Analysis/**/*.lean file is reachable from Analysis.lean would have caught this at the moment Section 1.4 was added, and would stop it recurring.

Scope widened after an audit

Checking by .olean presence (the reliable test — lean_lib with no globs builds only Analysis.lean's closure, so a plain grep of the import list is misleading) turned up two more never-compiled modules, Section_1_4_4 and Section_1_4_5. Both already compile, so they just needed importing. Final build: 8315 jobs, no errors, and every file under Analysis/ except one is now in the closure.

The exception is Analysis/Misc/equational.lean, which cannot simply be added: it declares a top-level S that collides with Analysis.Misc.erdos_379, so importing it fails with environment already contains 'S'. It needs a rename or a namespace first, which seemed out of scope here.

Also included: a .gitignore entry for __pycache__, which the test suite added in #731-#735 creates on first run.

🤖 Generated with Claude Code