feat(MeasureTheory): prove elementary and Jordan product measures - #665

Open

Chessing234 wants to merge 8 commits into

teorth:mainfrom

Chessing234:measure-elementary-prod

Commits on Aug 25, 2026

feat(MeasureTheory): prove the product of elementary sets is elementary
Chessing234
committed
2ebb2a1
feat(MeasureTheory): prove Jordan measure is multiplicative on products
Chessing234
committed
d03b804
fix(MeasureTheory): close the product lemmas without convert/simp loops
Chessing234
committed
50630c0
fix(MeasureTheory): avoid dependent rewrites in the product lemmas
Chessing234
committed
022f962
fix(MeasureTheory): match prod_equiv toFun indices in the product lemmas
Chessing234
committed
4a21fb4
fix(MeasureTheory): rewrite the product-box side via Fin.eq_of_val_eq
Chessing234
committed
5205895
fix(MeasureTheory): control the product error with a δ that scales with the measures
Chessing234
committed
930f9d1

Commits on Aug 29, 2026

fix prod norm proof to match Fin.castAdd/natAdd indices
Chessing234
committed
f018a92