Skip to content

Commit 07ee0f0

Browse files
committed
chore(MeasureTheory/VectorMeasure/Decomposition/RadonNikodym): remove an erw (#38418)
- rewrites `withDensityᵥ_rnDeriv_eq` to replace `erw [VectorMeasure.sub_apply]` with a plain `rw` - adds `JordanDecomposition.toSignedMeasure` to the same rewrite chain so the proof closes without `erw` Extracted from #38415 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
1 parent 7ca8bd0 commit 07ee0f0

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,8 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm
3434
rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
3535
setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]
3636
· conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
37-
erw [VectorMeasure.sub_apply]
38-
rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
37+
rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
38+
toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
3939
measureReal_def]
4040
all_goals
4141
refine Integrable.integrableOn ?_

0 commit comments

Comments
 (0)