[GOAL]
α : Type u_1
X Y : Discrete α
⊢ Fintype (X ⟶ Y)
[PROOFSTEP]
apply ULift.fintype


[GOAL]
ι : Type u_1
inst✝ : Fintype ι
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
[PROOFSTEP]
haveI : IsAddLeftInvariant StieltjesFunction.id.measure :=
  ⟨fun a =>
    Eq.symm <|
      Real.measure_ext_Ioo_rat fun p q => by
        simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo, sub_sub_sub_cancel_right,
          StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim, StieltjesFunction.id_apply, id.def,
          preimage_const_add_Ioo]⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
p q : ℚ
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (Ioo ↑p ↑q) =
    ↑↑(Measure.map (fun x => a + x) (StieltjesFunction.measure StieltjesFunction.id)) (Ioo ↑p ↑q)
[PROOFSTEP]
simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo, sub_sub_sub_cancel_right,
  StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim, StieltjesFunction.id_apply, id.def,
  preimage_const_add_Ioo]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
[PROOFSTEP]
have A : StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1 :=
  by
  change StieltjesFunction.id.measure (parallelepiped (stdOrthonormalBasis ℝ ℝ)) = 1
  rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H) <;>
    simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id.def, tsub_zero,
      StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
[PROOFSTEP]
change StieltjesFunction.id.measure (parallelepiped (stdOrthonormalBasis ℝ ℝ)) = 1
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (parallelepiped ↑(stdOrthonormalBasis ℝ ℝ)) = 1
[PROOFSTEP]
rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H)
[GOAL]
case inl
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
H : parallelepiped ↑(stdOrthonormalBasis ℝ ℝ) = Icc 0 1
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (parallelepiped ↑(stdOrthonormalBasis ℝ ℝ)) = 1
[PROOFSTEP]
simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id.def, tsub_zero,
  StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]
[GOAL]
case inr
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
H : parallelepiped ↑(stdOrthonormalBasis ℝ ℝ) = Icc (-1) 0
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (parallelepiped ↑(stdOrthonormalBasis ℝ ℝ)) = 1
[PROOFSTEP]
simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id.def, tsub_zero,
  StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
[PROOFSTEP]
conv_rhs => rw [addHaarMeasure_unique StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
| StieltjesFunction.measure StieltjesFunction.id
[PROOFSTEP]
rw [addHaarMeasure_unique StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
| StieltjesFunction.measure StieltjesFunction.id
[PROOFSTEP]
rw [addHaarMeasure_unique StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
| StieltjesFunction.measure StieltjesFunction.id
[PROOFSTEP]
rw [addHaarMeasure_unique StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
⊢ volume = 1 • addHaarMeasure (Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ)))
[PROOFSTEP]
simp only [volume, Basis.addHaar, one_smul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
s : Set ℝ
⊢ ↑↑volume s = ↑↑(StieltjesFunction.measure StieltjesFunction.id) s
[PROOFSTEP]
simp [volume_eq_stieltjes_id]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ℝ
⊢ ↑↑volume (Ico a b) = ofReal (b - a)
[PROOFSTEP]
simp [volume_val]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ℝ
⊢ ↑↑volume (Icc a b) = ofReal (b - a)
[PROOFSTEP]
simp [volume_val]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ℝ
⊢ ↑↑volume (Ioo a b) = ofReal (b - a)
[PROOFSTEP]
simp [volume_val]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ℝ
⊢ ↑↑volume (Ioc a b) = ofReal (b - a)
[PROOFSTEP]
simp [volume_val]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume {a} = 0
[PROOFSTEP]
simp [volume_val]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
r : ℝ≥0
⊢ ↑r = ↑↑volume (Icc 0 ↑r)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a r : ℝ
⊢ ↑↑volume (Metric.ball a r) = ofReal (2 * r)
[PROOFSTEP]
rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel', two_mul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a r : ℝ
⊢ ↑↑volume (Metric.closedBall a r) = ofReal (2 * r)
[PROOFSTEP]
rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel', two_mul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
⊢ ↑↑volume (EMetric.ball a r) = 2 * r
[PROOFSTEP]
rcases eq_or_ne r ∞ with (rfl | hr)
[GOAL]
case inl
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (EMetric.ball a ⊤) = 2 * ⊤
[PROOFSTEP]
rw [Metric.emetric_ball_top, volume_univ, two_mul, _root_.top_add]
[GOAL]
case inr
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ ↑↑volume (EMetric.ball a r) = 2 * r
[PROOFSTEP]
lift r to ℝ≥0 using hr
[GOAL]
case inr.intro
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0
⊢ ↑↑volume (EMetric.ball a ↑r) = 2 * ↑r
[PROOFSTEP]
rw [Metric.emetric_ball_nnreal, volume_ball, two_mul, ← NNReal.coe_add, ENNReal.ofReal_coe_nnreal, ENNReal.coe_add,
  two_mul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
⊢ ↑↑volume (EMetric.closedBall a r) = 2 * r
[PROOFSTEP]
rcases eq_or_ne r ∞ with (rfl | hr)
[GOAL]
case inl
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (EMetric.closedBall a ⊤) = 2 * ⊤
[PROOFSTEP]
rw [EMetric.closedBall_top, volume_univ, two_mul, _root_.top_add]
[GOAL]
case inr
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ ↑↑volume (EMetric.closedBall a r) = 2 * r
[PROOFSTEP]
lift r to ℝ≥0 using hr
[GOAL]
case inr.intro
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0
⊢ ↑↑volume (EMetric.closedBall a ↑r) = 2 * ↑r
[PROOFSTEP]
rw [Metric.emetric_closedBall_nnreal, volume_closedBall, two_mul, ← NNReal.coe_add, ENNReal.ofReal_coe_nnreal,
  ENNReal.coe_add, two_mul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ℝ
⊢ ↑↑volume (uIcc a b) = ofReal |b - a|
[PROOFSTEP]
rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
n : ℕ
⊢ ↑n = ↑↑volume (Ioo a (a + ↑n))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Ici a) = ⊤
[PROOFSTEP]
rw [← measure_congr Ioi_ae_eq_Ici]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Ioi a) = ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
n : ℕ
⊢ ↑n = ↑↑volume (Ioo (a - ↑n) a)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Iic a) = ⊤
[PROOFSTEP]
rw [← measure_congr Iio_ae_eq_Iic]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Iio a) = ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
x : ℝ
⊢ ↑↑volume (Ioo (x - 1) (x + 1)) < ⊤
[PROOFSTEP]
simp only [Real.volume_Ioo, ENNReal.ofReal_lt_top]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
x y : ℝ
⊢ ↑↑(Measure.restrict volume (Icc x y)) univ < ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
x y : ℝ
⊢ ↑↑(Measure.restrict volume (Ico x y)) univ < ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
x y : ℝ
⊢ ↑↑(Measure.restrict volume (Ioc x y)) univ < ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
x y : ℝ
⊢ ↑↑(Measure.restrict volume (Ioo x y)) univ < ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
s : Set ℝ
⊢ ↑↑volume s ≤ EMetric.diam s
[PROOFSTEP]
by_cases hs : Metric.Bounded s
[GOAL]
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set ℝ
hs : Metric.Bounded s
⊢ ↑↑volume s ≤ EMetric.diam s
[PROOFSTEP]
rw [Real.ediam_eq hs, ← volume_Icc]
[GOAL]
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set ℝ
hs : Metric.Bounded s
⊢ ↑↑volume s ≤ ↑↑volume (Icc (sInf s) (sSup s))
[PROOFSTEP]
exact volume.mono (Real.subset_Icc_sInf_sSup_of_bounded hs)
[GOAL]
case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set ℝ
hs : ¬Metric.Bounded s
⊢ ↑↑volume s ≤ EMetric.diam s
[PROOFSTEP]
rw [Metric.ediam_of_unbounded hs]
[GOAL]
case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set ℝ
hs : ¬Metric.Bounded s
⊢ ↑↑volume s ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
⊢ 0 < ↑↑volume {x | p x}
[PROOFSTEP]
rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < ↑↑volume {x | p x}
[PROOFSTEP]
refine' lt_of_lt_of_le _ (measure_mono hs)
[GOAL]
case intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < ↑↑volume (Ioo l u)
[PROOFSTEP]
simpa [-mem_Ioo] using hx.1.trans hx.2
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ↑↑volume (Icc a b) = ∏ i : ι, ofReal (b i - a i)
[PROOFSTEP]
rw [← pi_univ_Icc, volume_pi_pi]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i : ι, ↑↑volume (Icc (a i) (b i)) = ∏ i : ι, ofReal (b i - a i)
[PROOFSTEP]
simp only [Real.volume_Icc]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal (↑↑volume (Icc a b)) = ∏ i : ι, (b i - a i)
[PROOFSTEP]
simp only [volume_Icc_pi, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal (↑↑volume (Set.pi univ fun i => Ioo (a i) (b i))) = ∏ i : ι, (b i - a i)
[PROOFSTEP]
simp only [volume_pi_Ioo, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal (↑↑volume (Set.pi univ fun i => Ioc (a i) (b i))) = ∏ i : ι, (b i - a i)
[PROOFSTEP]
simp only [volume_pi_Ioc, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal (↑↑volume (Set.pi univ fun i => Ico (a i) (b i))) = ∏ i : ι, (b i - a i)
[PROOFSTEP]
simp only [volume_pi_Ico, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ↑↑volume (Metric.ball a r) = ofReal ((2 * r) ^ Fintype.card ι)
[PROOFSTEP]
simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ofReal (2 * r) ^ Finset.card Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
[PROOFSTEP]
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ↑↑volume (Metric.closedBall a r) = ofReal ((2 * r) ^ Fintype.card ι)
[PROOFSTEP]
simp only [MeasureTheory.volume_pi_closedBall a hr, volume_closedBall, Finset.prod_const]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.card Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
[PROOFSTEP]
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr) _).symm
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
⊢ ∏ _i : ι, ↑1 * EMetric.diam s = EMetric.diam s ^ Fintype.card ι
[PROOFSTEP]
simp only [ENNReal.coe_one, one_mul, Finset.prod_const, Fintype.card]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
⊢ ofReal |a| • Measure.map (fun x => a * x) volume = volume
[PROOFSTEP]
refine' (Real.measure_ext_Ioo_rat fun p q => _).symm
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
p q : ℚ
⊢ ↑↑volume (Ioo ↑p ↑q) = ↑↑(ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
[PROOFSTEP]
cases' lt_or_gt_of_ne h with h h
[GOAL]
case inl
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a < 0
⊢ ↑↑volume (Ioo ↑p ↑q) = ↑↑(ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
[PROOFSTEP]
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt <| neg_pos.2 h),
  Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, neg_sub_neg, neg_mul,
  preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul, mul_div_cancel' _ (ne_of_lt h)]
[GOAL]
case inr
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a > 0
⊢ ↑↑volume (Ioo ↑p ↑q) = ↑↑(ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
[PROOFSTEP]
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt h),
  Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, preimage_const_mul_Ioo _ _ h, abs_of_pos h, mul_sub,
  mul_div_cancel' _ (ne_of_gt h), smul_eq_mul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun x => a * x) volume = ofReal |a⁻¹| • volume
[PROOFSTEP]
conv_rhs =>
  rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h,
    abs_one, ENNReal.ofReal_one, one_smul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
| ofReal |a⁻¹| • volume
[PROOFSTEP]
rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h,
    abs_one, ENNReal.ofReal_one, one_smul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
| ofReal |a⁻¹| • volume
[PROOFSTEP]
rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h,
    abs_one, ENNReal.ofReal_one, one_smul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
| ofReal |a⁻¹| • volume
[PROOFSTEP]
rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h,
  abs_one, ENNReal.ofReal_one, one_smul]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(Measure.map (fun x => a * x) volume) s = ofReal |a⁻¹| * ↑↑volume s
[PROOFSTEP]
rw [map_volume_mul_left h]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * ↑↑volume s
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
⊢ ofReal |a| • Measure.map (fun x => x * a) volume = volume
[PROOFSTEP]
simpa only [mul_comm] using Real.smul_map_volume_mul_left h
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun x => x * a) volume = ofReal |a⁻¹| • volume
[PROOFSTEP]
simpa only [mul_comm] using Real.map_volume_mul_left h
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(Measure.map (fun x => x * a) volume) s = ofReal |a⁻¹| * ↑↑volume s
[PROOFSTEP]
rw [map_volume_mul_right h]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * ↑↑volume s
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
⊢ ofReal |det (Matrix.diagonal D)| • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume = volume
[PROOFSTEP]
refine' (Measure.pi_eq fun s hs => _).symm
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(ofReal |det (Matrix.diagonal D)| • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume) (Set.pi univ s) =
    ∏ i : ι, ↑↑volume (s i)
[PROOFSTEP]
simp only [det_diagonal, Measure.coe_smul, Algebra.id.smul_eq_mul, Pi.smul_apply]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i : ι, D i| * ↑↑(Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume) (Set.pi univ s) =
    ∏ x : ι, ↑↑volume (s x)
[PROOFSTEP]
rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i : ι, D i| * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ↑(↑toLin' (Matrix.diagonal D))
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ↑(↑toLin' (Matrix.diagonal D))
[PROOFSTEP]
exact Continuous.measurable (LinearMap.continuous_on_pi _)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i : ι, D i| * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)
[PROOFSTEP]
have :
  (Matrix.toLin' (diagonal D) ⁻¹' Set.pi Set.univ fun i : ι => s i) = Set.pi Set.univ fun i : ι => (D i * ·) ⁻¹' s i :=
  by
  ext f
  simp only [LinearMap.coe_proj, Algebra.id.smul_eq_mul, LinearMap.smul_apply, mem_univ_pi, mem_preimage,
    LinearMap.pi_apply, diagonal_toLin']
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
[PROOFSTEP]
ext f
[GOAL]
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
f : ι → ℝ
⊢ (f ∈ ↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) ↔
    f ∈ Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
[PROOFSTEP]
simp only [LinearMap.coe_proj, Algebra.id.smul_eq_mul, LinearMap.smul_apply, mem_univ_pi, mem_preimage,
  LinearMap.pi_apply, diagonal_toLin']
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
⊢ ofReal |∏ i : ι, D i| * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)
[PROOFSTEP]
have B : ∀ i, ofReal (abs (D i)) * volume ((D i * ·) ⁻¹' s i) = volume (s i) :=
  by
  intro i
  have A : D i ≠ 0 := by
    simp only [det_diagonal, Ne.def] at h
    exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
  rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_inv_cancel A,
    abs_one, ENNReal.ofReal_one, one_mul]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
⊢ ∀ (i : ι), ofReal |D i| * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
⊢ ofReal |D i| * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
[PROOFSTEP]
have A : D i ≠ 0 := by
  simp only [det_diagonal, Ne.def] at h
  exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
⊢ D i ≠ 0
[PROOFSTEP]
simp only [det_diagonal, Ne.def] at h
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
h : ¬∏ i : ι, D i = 0
⊢ D i ≠ 0
[PROOFSTEP]
exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal |D i| * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
[PROOFSTEP]
rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_inv_cancel A, abs_one,
  ENNReal.ofReal_one, one_mul]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
⊢ ofReal |∏ i : ι, D i| * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)
[PROOFSTEP]
rw [this, volume_pi_pi, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ←
  Finset.prod_mul_distrib]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
⊢ ∏ x : ι, ofReal |D x| * ↑↑volume ((fun x_1 => D x * x_1) ⁻¹' s x) = ∏ x : ι, ↑↑volume (s x)
[PROOFSTEP]
simp only [B]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
let p : ι → Prop := fun i => i ≠ t.i
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
let α : Type _ := { x // p x }
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
let β : Type _ := { x // ¬p x }
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
let g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun _ => t.c * a ⟨t.j, t.hij.symm⟩) + b
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
let F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.1, g p.1 p.2)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
let e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun _ : ι => ℝ) p
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
have : (toLin' t.toMatrix : (ι → ℝ) → ι → ℝ) = e.symm ∘ F ∘ e := by
  cases t with
  | mk t_i t_j t_hij t_c =>
    ext f k
    simp only [LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not, Algebra.id.smul_eq_mul, one_mul,
      dotProduct, stdBasisMatrix, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply,
      zero_mul, LinearMap.smul_apply, Function.comp_apply, MeasurableEquiv.piEquivPiSubtypeProd_apply,
      Matrix.TransvectionStruct.toMatrix_mk, Matrix.mulVec, LinearEquiv.map_add, ite_mul, Matrix.toLin'_apply,
      Pi.smul_apply, Subtype.coe_mk, LinearMap.add_apply, Finset.sum_congr, Matrix.toLin'_one]
    by_cases h : t_i = k
    ·
      simp only [h, true_and_iff, Finset.mem_univ, if_true, eq_self_iff_true, Finset.sum_ite_eq, one_apply, boole_mul,
        add_comm]
    · simp only [h, Ne.symm h, add_zero, if_false, Finset.sum_const_zero, false_and_iff, mul_zero]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
⊢ ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
[PROOFSTEP]
cases t with
| mk t_i t_j t_hij t_c =>
  ext f k
  simp only [LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not, Algebra.id.smul_eq_mul, one_mul, dotProduct,
    stdBasisMatrix, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply, zero_mul,
    LinearMap.smul_apply, Function.comp_apply, MeasurableEquiv.piEquivPiSubtypeProd_apply,
    Matrix.TransvectionStruct.toMatrix_mk, Matrix.mulVec, LinearEquiv.map_add, ite_mul, Matrix.toLin'_apply,
    Pi.smul_apply, Subtype.coe_mk, LinearMap.add_apply, Finset.sum_congr, Matrix.toLin'_one]
  by_cases h : t_i = k
  ·
    simp only [h, true_and_iff, Finset.mem_univ, if_true, eq_self_iff_true, Finset.sum_ite_eq, one_apply, boole_mul,
      add_comm]
  · simp only [h, Ne.symm h, add_zero, if_false, Finset.sum_const_zero, false_and_iff, mul_zero]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
⊢ ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
[PROOFSTEP]
cases t with
| mk t_i t_j t_hij t_c =>
  ext f k
  simp only [LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not, Algebra.id.smul_eq_mul, one_mul, dotProduct,
    stdBasisMatrix, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply, zero_mul,
    LinearMap.smul_apply, Function.comp_apply, MeasurableEquiv.piEquivPiSubtypeProd_apply,
    Matrix.TransvectionStruct.toMatrix_mk, Matrix.mulVec, LinearEquiv.map_add, ite_mul, Matrix.toLin'_apply,
    Pi.smul_apply, Subtype.coe_mk, LinearMap.add_apply, Finset.sum_congr, Matrix.toLin'_one]
  by_cases h : t_i = k
  ·
    simp only [h, true_and_iff, Finset.mem_univ, if_true, eq_self_iff_true, Finset.sum_ite_eq, one_apply, boole_mul,
      add_comm]
  · simp only [h, Ne.symm h, add_zero, if_false, Finset.sum_const_zero, false_and_iff, mul_zero]
[GOAL]
case mk
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
p : ι → Prop := fun i => i ≠ { i := t_i, j := t_j, hij := t_hij, c := t_c }.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ :=
  fun a b =>
    (fun x =>
        { i := t_i, j := t_j, hij := t_hij, c := t_c }.c *
          a
            { val := { i := t_i, j := t_j, hij := t_hij, c := t_c }.j,
              property :=
                (_ :
                  { i := t_i, j := t_j, hij := t_hij, c := t_c }.j ≠
                    { i := t_i, j := t_j, hij := t_hij, c := t_c }.i) }) +
      b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
⊢ ↑(↑toLin' (TransvectionStruct.toMatrix { i := t_i, j := t_j, hij := t_hij, c := t_c })) =
    ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
[PROOFSTEP]

| mk t_i t_j t_hij t_c =>
  ext f k
  simp only [LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not, Algebra.id.smul_eq_mul, one_mul, dotProduct,
    stdBasisMatrix, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply, zero_mul,
    LinearMap.smul_apply, Function.comp_apply, MeasurableEquiv.piEquivPiSubtypeProd_apply,
    Matrix.TransvectionStruct.toMatrix_mk, Matrix.mulVec, LinearEquiv.map_add, ite_mul, Matrix.toLin'_apply,
    Pi.smul_apply, Subtype.coe_mk, LinearMap.add_apply, Finset.sum_congr, Matrix.toLin'_one]
  by_cases h : t_i = k
  ·
    simp only [h, true_and_iff, Finset.mem_univ, if_true, eq_self_iff_true, Finset.sum_ite_eq, one_apply, boole_mul,
      add_comm]
  · simp only [h, Ne.symm h, add_zero, if_false, Finset.sum_const_zero, false_and_iff, mul_zero]
[GOAL]
case mk
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
p : ι → Prop := fun i => i ≠ { i := t_i, j := t_j, hij := t_hij, c := t_c }.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ :=
  fun a b =>
    (fun x =>
        { i := t_i, j := t_j, hij := t_hij, c := t_c }.c *
          a
            { val := { i := t_i, j := t_j, hij := t_hij, c := t_c }.j,
              property :=
                (_ :
                  { i := t_i, j := t_j, hij := t_hij, c := t_c }.j ≠
                    { i := t_i, j := t_j, hij := t_hij, c := t_c }.i) }) +
      b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
⊢ ↑(↑toLin' (TransvectionStruct.toMatrix { i := t_i, j := t_j, hij := t_hij, c := t_c })) =
    ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
[PROOFSTEP]
ext f k
[GOAL]
case mk.h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
p : ι → Prop := fun i => i ≠ { i := t_i, j := t_j, hij := t_hij, c := t_c }.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ :=
  fun a b =>
    (fun x =>
        { i := t_i, j := t_j, hij := t_hij, c := t_c }.c *
          a
            { val := { i := t_i, j := t_j, hij := t_hij, c := t_c }.j,
              property :=
                (_ :
                  { i := t_i, j := t_j, hij := t_hij, c := t_c }.j ≠
                    { i := t_i, j := t_j, hij := t_hij, c := t_c }.i) }) +
      b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
f : ι → ℝ
k : ι
⊢ ↑(↑toLin' (TransvectionStruct.toMatrix { i := t_i, j := t_j, hij := t_hij, c := t_c })) f k =
    (↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e) f k
[PROOFSTEP]
simp only [LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not, Algebra.id.smul_eq_mul, one_mul, dotProduct,
  stdBasisMatrix, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply, zero_mul,
  LinearMap.smul_apply, Function.comp_apply, MeasurableEquiv.piEquivPiSubtypeProd_apply,
  Matrix.TransvectionStruct.toMatrix_mk, Matrix.mulVec, LinearEquiv.map_add, ite_mul, Matrix.toLin'_apply,
  Pi.smul_apply, Subtype.coe_mk, LinearMap.add_apply, Finset.sum_congr, Matrix.toLin'_one]
[GOAL]
case mk.h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
p : ι → Prop := fun i => i ≠ { i := t_i, j := t_j, hij := t_hij, c := t_c }.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ :=
  fun a b =>
    (fun x =>
        { i := t_i, j := t_j, hij := t_hij, c := t_c }.c *
          a
            { val := { i := t_i, j := t_j, hij := t_hij, c := t_c }.j,
              property :=
                (_ :
                  { i := t_i, j := t_j, hij := t_hij, c := t_c }.j ≠
                    { i := t_i, j := t_j, hij := t_hij, c := t_c }.i) }) +
      b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
f : ι → ℝ
k : ι
⊢ (f k + ∑ x : ι, if t_i = k ∧ t_j = x then t_c * f x else 0) = if k = t_i then t_c * f t_j + f k else f k
[PROOFSTEP]
by_cases h : t_i = k
[GOAL]
case pos
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
p : ι → Prop := fun i => i ≠ { i := t_i, j := t_j, hij := t_hij, c := t_c }.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ :=
  fun a b =>
    (fun x =>
        { i := t_i, j := t_j, hij := t_hij, c := t_c }.c *
          a
            { val := { i := t_i, j := t_j, hij := t_hij, c := t_c }.j,
              property :=
                (_ :
                  { i := t_i, j := t_j, hij := t_hij, c := t_c }.j ≠
                    { i := t_i, j := t_j, hij := t_hij, c := t_c }.i) }) +
      b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
f : ι → ℝ
k : ι
h : t_i = k
⊢ (f k + ∑ x : ι, if t_i = k ∧ t_j = x then t_c * f x else 0) = if k = t_i then t_c * f t_j + f k else f k
[PROOFSTEP]
simp only [h, true_and_iff, Finset.mem_univ, if_true, eq_self_iff_true, Finset.sum_ite_eq, one_apply, boole_mul,
  add_comm]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
p : ι → Prop := fun i => i ≠ { i := t_i, j := t_j, hij := t_hij, c := t_c }.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ :=
  fun a b =>
    (fun x =>
        { i := t_i, j := t_j, hij := t_hij, c := t_c }.c *
          a
            { val := { i := t_i, j := t_j, hij := t_hij, c := t_c }.j,
              property :=
                (_ :
                  { i := t_i, j := t_j, hij := t_hij, c := t_c }.j ≠
                    { i := t_i, j := t_j, hij := t_hij, c := t_c }.i) }) +
      b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
f : ι → ℝ
k : ι
h : ¬t_i = k
⊢ (f k + ∑ x : ι, if t_i = k ∧ t_j = x then t_c * f x else 0) = if k = t_i then t_c * f t_j + f k else f k
[PROOFSTEP]
simp only [h, Ne.symm h, add_zero, if_false, Finset.sum_const_zero, false_and_iff, mul_zero]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
⊢ MeasurePreserving ↑(↑toLin' (TransvectionStruct.toMatrix t))
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
⊢ MeasurePreserving (↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e)
[PROOFSTEP]
have A : MeasurePreserving e := by convert volume_preserving_piEquivPiSubtypeProd (fun _ : ι => ℝ) p
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
⊢ MeasurePreserving ↑e
[PROOFSTEP]
convert volume_preserving_piEquivPiSubtypeProd (fun _ : ι => ℝ) p
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
A : MeasurePreserving ↑e
⊢ MeasurePreserving (↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e)
[PROOFSTEP]
have B : MeasurePreserving F :=
  haveI g_meas : Measurable (Function.uncurry g) :=
    by
    have : Measurable fun c : α → ℝ => c ⟨t.j, t.hij.symm⟩ := measurable_pi_apply ⟨t.j, t.hij.symm⟩
    refine Measurable.add ?_ measurable_snd
    refine measurable_pi_lambda _ fun _ => Measurable.const_mul ?_ _
    exact this.comp measurable_fst
  (MeasurePreserving.id _).skew_product g_meas
    (eventually_of_forall fun a =>
      map_add_left_eq_self (Measure.pi fun _ => (stdOrthonormalBasis ℝ ℝ).toBasis.addHaar) _)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
A : MeasurePreserving ↑e
⊢ Measurable (Function.uncurry g)
[PROOFSTEP]
have : Measurable fun c : α → ℝ => c ⟨t.j, t.hij.symm⟩ := measurable_pi_apply ⟨t.j, t.hij.symm⟩
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this✝ : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
A : MeasurePreserving ↑e
this : Measurable fun c => c { val := t.j, property := (_ : t.j ≠ t.i) }
⊢ Measurable (Function.uncurry g)
[PROOFSTEP]
refine Measurable.add ?_ measurable_snd
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this✝ : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
A : MeasurePreserving ↑e
this : Measurable fun c => c { val := t.j, property := (_ : t.j ≠ t.i) }
⊢ Measurable fun a x => t.c * Prod.fst a { val := t.j, property := (_ : t.j ≠ t.i) }
[PROOFSTEP]
refine measurable_pi_lambda _ fun _ => Measurable.const_mul ?_ _
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this✝ : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
A : MeasurePreserving ↑e
this : Measurable fun c => c { val := t.j, property := (_ : t.j ≠ t.i) }
x✝ : β
⊢ Measurable fun c => Prod.fst c { val := t.j, property := (_ : t.j ≠ t.i) }
[PROOFSTEP]
exact this.comp measurable_fst
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
p : ι → Prop := fun i => i ≠ t.i
α : Type u_1 := { x // p x }
β : Type u_1 := { x // ¬p x }
g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun x => t.c * a { val := t.j, property := (_ : t.j ≠ t.i) }) + b
F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.fst, g p.fst p.snd)
e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun x => ℝ) p
this : ↑(↑toLin' (TransvectionStruct.toMatrix t)) = ↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e
A : MeasurePreserving ↑e
B : MeasurePreserving F
⊢ MeasurePreserving (↑(MeasurableEquiv.symm e) ∘ F ∘ ↑e)
[PROOFSTEP]
exact ((A.symm e).comp B).comp A
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
⊢ Measure.map (↑(↑toLin' M)) volume = ofReal |(det M)⁻¹| • volume
[PROOFSTEP]
apply diagonal_transvection_induction_of_det_ne_zero _ M hM
[GOAL]
case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
⊢ ∀ (D : ι → ℝ),
    det (Matrix.diagonal D) ≠ 0 →
      Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume = ofReal |(det (Matrix.diagonal D))⁻¹| • volume
[PROOFSTEP]
intro D hD
[GOAL]
case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
D : ι → ℝ
hD : det (Matrix.diagonal D) ≠ 0
⊢ Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume = ofReal |(det (Matrix.diagonal D))⁻¹| • volume
[PROOFSTEP]
conv_rhs => rw [← smul_map_diagonal_volume_pi hD]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
D : ι → ℝ
hD : det (Matrix.diagonal D) ≠ 0
| ofReal |(det (Matrix.diagonal D))⁻¹| • volume
[PROOFSTEP]
rw [← smul_map_diagonal_volume_pi hD]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
D : ι → ℝ
hD : det (Matrix.diagonal D) ≠ 0
| ofReal |(det (Matrix.diagonal D))⁻¹| • volume
[PROOFSTEP]
rw [← smul_map_diagonal_volume_pi hD]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
D : ι → ℝ
hD : det (Matrix.diagonal D) ≠ 0
| ofReal |(det (Matrix.diagonal D))⁻¹| • volume
[PROOFSTEP]
rw [← smul_map_diagonal_volume_pi hD]
[GOAL]
case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
D : ι → ℝ
hD : det (Matrix.diagonal D) ≠ 0
⊢ Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume =
    ofReal |(det (Matrix.diagonal D))⁻¹| •
      ofReal |det (Matrix.diagonal D)| • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume
[PROOFSTEP]
rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel hD, abs_one, ENNReal.ofReal_one, one_smul]
[GOAL]
case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
⊢ ∀ (t : TransvectionStruct ι ℝ),
    Measure.map (↑(↑toLin' (TransvectionStruct.toMatrix t))) volume =
      ofReal |(det (TransvectionStruct.toMatrix t))⁻¹| • volume
[PROOFSTEP]
intro t
[GOAL]
case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
t : TransvectionStruct ι ℝ
⊢ Measure.map (↑(↑toLin' (TransvectionStruct.toMatrix t))) volume =
    ofReal |(det (TransvectionStruct.toMatrix t))⁻¹| • volume
[PROOFSTEP]
simp only [Matrix.TransvectionStruct.det, ENNReal.ofReal_one, (volume_preserving_transvectionStruct _).map_eq, one_smul,
  _root_.inv_one, abs_one]
[GOAL]
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
⊢ ∀ (A B : Matrix ι ι ℝ),
    det A ≠ 0 →
      det B ≠ 0 →
        Measure.map (↑(↑toLin' A)) volume = ofReal |(det A)⁻¹| • volume →
          Measure.map (↑(↑toLin' B)) volume = ofReal |(det B)⁻¹| • volume →
            Measure.map (↑(↑toLin' (A * B))) volume = ofReal |(det (A * B))⁻¹| • volume
[PROOFSTEP]
intro A B _ _ IHA IHB
[GOAL]
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : det A ≠ 0
a✝ : det B ≠ 0
IHA : Measure.map (↑(↑toLin' A)) volume = ofReal |(det A)⁻¹| • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal |(det B)⁻¹| • volume
⊢ Measure.map (↑(↑toLin' (A * B))) volume = ofReal |(det (A * B))⁻¹| • volume
[PROOFSTEP]
rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA, smul_smul, ←
  ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv]
[GOAL]
case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : det A ≠ 0
a✝ : det B ≠ 0
IHA : Measure.map (↑(↑toLin' A)) volume = ofReal |(det A)⁻¹| • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal |(det B)⁻¹| • volume
⊢ Measurable ↑(↑toLin' A)
[PROOFSTEP]
apply Continuous.measurable
[GOAL]
case hmul.hg.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : det A ≠ 0
a✝ : det B ≠ 0
IHA : Measure.map (↑(↑toLin' A)) volume = ofReal |(det A)⁻¹| • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal |(det B)⁻¹| • volume
⊢ Continuous ↑(↑toLin' A)
[PROOFSTEP]
apply LinearMap.continuous_on_pi
[GOAL]
case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : det A ≠ 0
a✝ : det B ≠ 0
IHA : Measure.map (↑(↑toLin' A)) volume = ofReal |(det A)⁻¹| • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal |(det B)⁻¹| • volume
⊢ Measurable ↑(↑toLin' B)
[PROOFSTEP]
apply Continuous.measurable
[GOAL]
case hmul.hf.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : det A ≠ 0
a✝ : det B ≠ 0
IHA : Measure.map (↑(↑toLin' A)) volume = ofReal |(det A)⁻¹| • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal |(det B)⁻¹| • volume
⊢ Continuous ↑(↑toLin' B)
[PROOFSTEP]
apply LinearMap.continuous_on_pi
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
⊢ Measure.map (↑f) volume = ofReal |(↑LinearMap.det f)⁻¹| • volume
[PROOFSTEP]
classical
  -- this is deduced from the matrix case
let M := LinearMap.toMatrix' f
have A : LinearMap.det f = det M := by simp only [LinearMap.det_toMatrix']
have B : f = toLin' M := by simp only [toLin'_toMatrix']
rw [A, B]
apply map_matrix_volume_pi_eq_smul_volume_pi
rwa [A] at hf
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
⊢ Measure.map (↑f) volume = ofReal |(↑LinearMap.det f)⁻¹| • volume
[PROOFSTEP]
let M := LinearMap.toMatrix' f
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
⊢ Measure.map (↑f) volume = ofReal |(↑LinearMap.det f)⁻¹| • volume
[PROOFSTEP]
have A : LinearMap.det f = det M := by simp only [LinearMap.det_toMatrix']
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
⊢ ↑LinearMap.det f = det M
[PROOFSTEP]
simp only [LinearMap.det_toMatrix']
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
A : ↑LinearMap.det f = det M
⊢ Measure.map (↑f) volume = ofReal |(↑LinearMap.det f)⁻¹| • volume
[PROOFSTEP]
have B : f = toLin' M := by simp only [toLin'_toMatrix']
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
A : ↑LinearMap.det f = det M
⊢ f = ↑toLin' M
[PROOFSTEP]
simp only [toLin'_toMatrix']
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
A : ↑LinearMap.det f = det M
B : f = ↑toLin' M
⊢ Measure.map (↑f) volume = ofReal |(↑LinearMap.det f)⁻¹| • volume
[PROOFSTEP]
rw [A, B]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
A : ↑LinearMap.det f = det M
B : f = ↑toLin' M
⊢ Measure.map (↑(↑toLin' M)) volume = ofReal |(det M)⁻¹| • volume
[PROOFSTEP]
apply map_matrix_volume_pi_eq_smul_volume_pi
[GOAL]
case hM
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
M : (fun x => Matrix ι ι ℝ) f := ↑LinearMap.toMatrix' f
A : ↑LinearMap.det f = det M
B : f = ↑toLin' M
⊢ det M ≠ 0
[PROOFSTEP]
rwa [A] at hf
[GOAL]
α : Type u_1
f g : α → ℝ
s : Set α
⊢ regionBetween f g s ⊆ s ×ˢ univ
[PROOFSTEP]
simpa only [prod_univ, regionBetween, Set.preimage, setOf_subset_setOf] using fun a => And.left
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
[PROOFSTEP]
dsimp only [regionBetween, Ioo, mem_setOf_eq, setOf_and]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.fst ∈ s} ∩ {a | a.snd ∈ {a_1 | f a.fst < a_1} ∩ {a_1 | a_1 < g a.fst}})
[PROOFSTEP]
refine'
  MeasurableSet.inter _
    ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_lt measurable_snd (hg.comp measurable_fst)))
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.fst ∈ s}
[PROOFSTEP]
exact measurable_fst hs
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.fst ∈ s ∧ p.snd ∈ Ioc (f p.fst) (g p.fst)}
[PROOFSTEP]
dsimp only [regionBetween, Ioc, mem_setOf_eq, setOf_and]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.fst ∈ s} ∩ {a | a.snd ∈ {a_1 | f a.fst < a_1} ∩ {a_1 | a_1 ≤ g a.fst}})
[PROOFSTEP]
refine'
  MeasurableSet.inter _
    ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_le measurable_snd (hg.comp measurable_fst)))
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.fst ∈ s}
[PROOFSTEP]
exact measurable_fst hs
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.fst ∈ s ∧ p.snd ∈ Ico (f p.fst) (g p.fst)}
[PROOFSTEP]
dsimp only [regionBetween, Ico, mem_setOf_eq, setOf_and]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.fst ∈ s} ∩ {a | a.snd ∈ {a_1 | f a.fst ≤ a_1} ∩ {a_1 | a_1 < g a.fst}})
[PROOFSTEP]
refine'
  MeasurableSet.inter _
    ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_lt measurable_snd (hg.comp measurable_fst)))
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.fst ∈ s}
[PROOFSTEP]
exact measurable_fst hs
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.fst ∈ s ∧ p.snd ∈ Icc (f p.fst) (g p.fst)}
[PROOFSTEP]
dsimp only [regionBetween, Icc, mem_setOf_eq, setOf_and]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.fst ∈ s} ∩ {a | a.snd ∈ {a_1 | f a.fst ≤ a_1} ∩ {a_1 | a_1 ≤ g a.fst}})
[PROOFSTEP]
refine'
  MeasurableSet.inter _
    ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_le measurable_snd (hg.comp measurable_fst)))
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.fst ∈ s}
[PROOFSTEP]
exact measurable_fst hs
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
⊢ MeasurableSet {p | p.snd = f p.fst}
[PROOFSTEP]
simpa using measurableSet_region_between_cc hf hf MeasurableSet.univ
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
classical
rw [Measure.prod_apply]
· have h : (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ENNReal.ofReal (g x - f x) :=
    by
    funext x
    rw [indicator_apply]
    split_ifs with h
    · have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x) := by simp [h, Ioo]
      simp only [hx, Real.volume_Ioo, sub_zero]
    · have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅ := by simp [h]
      simp only [hx, measure_empty]
  dsimp only [regionBetween, preimage_setOf_eq]
  rw [h, lintegral_indicator] <;> simp only [hs, Pi.sub_apply]
· exact measurableSet_regionBetween hf hg hs
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
rw [Measure.prod_apply]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ↑↑volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
have h : (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ENNReal.ofReal (g x - f x) :=
  by
  funext x
  rw [indicator_apply]
  split_ifs with h
  · have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x) := by simp [h, Ioo]
    simp only [hx, Real.volume_Ioo, sub_zero]
  · have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅ := by simp [h]
    simp only [hx, measure_empty]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = indicator s (fun x => ofReal (g x - f x)) x
[PROOFSTEP]
rw [indicator_apply]
[GOAL]
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
[PROOFSTEP]
have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x) := by simp [h, Ioo]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
[PROOFSTEP]
simp [h, Ioo]
[GOAL]
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
[PROOFSTEP]
simp only [hx, Real.volume_Ioo, sub_zero]
[GOAL]
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
[PROOFSTEP]
have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅ := by simp [h]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
⊢ {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
[PROOFSTEP]
simp only [hx, measure_empty]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ ∫⁻ (x : α), ↑↑volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
dsimp only [regionBetween, preimage_setOf_eq]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ ∫⁻ (x : α), ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
rw [h, lintegral_indicator]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
simp only [hs, Pi.sub_apply]
[GOAL]
case hs
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ MeasurableSet s
[PROOFSTEP]
simp only [hs, Pi.sub_apply]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
[PROOFSTEP]
exact measurableSet_regionBetween hf hg hs
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
have h₁ :
  (fun y => ENNReal.ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y =>
    ENNReal.ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y) :=
  (hg.ae_eq_mk.sub hf.ae_eq_mk).fun_comp ENNReal.ofReal
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
have h₂ :
  (μ.restrict s).prod volume (regionBetween f g s) =
    (μ.restrict s).prod volume (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :=
  by
  apply measure_congr
  apply EventuallyEq.rfl.inter
  exact
    ((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
      (EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
[PROOFSTEP]
apply measure_congr
[GOAL]
case H
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ regionBetween f g s =ᶠ[ae (Measure.prod (Measure.restrict μ s) volume)]
    regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s
[PROOFSTEP]
apply EventuallyEq.rfl.inter
[GOAL]
case H
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (fun p => Ioo (f p.fst) (g p.fst) p.snd) =ᶠ[ae (Measure.prod (Measure.restrict μ s) volume)] fun p =>
    Ioo (AEMeasurable.mk f hf p.fst) (AEMeasurable.mk g hg p.fst) p.snd
[PROOFSTEP]
exact
  ((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
    (EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
[PROOFSTEP]
rw [lintegral_congr_ae h₁, ← volume_regionBetween_eq_lintegral' hf.measurable_mk hg.measurable_mk hs]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) =
    ↑↑(Measure.prod μ volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
[PROOFSTEP]
convert h₂ using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s)
[PROOFSTEP]
rw [Measure.restrict_prod_eq_prod_univ]
[GOAL]
case h.e'_2
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) =
    ↑↑(Measure.restrict (Measure.prod μ volume) (s ×ˢ univ)) (regionBetween f g s)
[PROOFSTEP]
exact (Measure.restrict_eq_self _ (regionBetween_subset f g s)).symm
[GOAL]
case h.e'_3
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ ↑↑(Measure.prod μ volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
[PROOFSTEP]
rw [Measure.restrict_prod_eq_prod_univ]
[GOAL]
case h.e'_3
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
hf : AEMeasurable f
hg : AEMeasurable g
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun y =>
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween f g s) =
    ↑↑(Measure.prod (Measure.restrict μ s) volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ ↑↑(Measure.prod μ volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) =
    ↑↑(Measure.restrict (Measure.prod μ volume) (s ×ˢ univ))
      (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
[PROOFSTEP]
exact (Measure.restrict_eq_self _ (regionBetween_subset (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)).symm
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
[PROOFSTEP]
let T : s × s → Set ℝ := fun p => Ioo p.1 p.2
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
[PROOFSTEP]
let u := ⋃ i : ↥s × ↥s, T i
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
[PROOFSTEP]
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
[PROOFSTEP]
obtain ⟨A, A_count, hA⟩ : ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
  isOpen_iUnion_countable _ fun p => isOpen_Ioo
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
[PROOFSTEP]
have : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p := by
  intro x hx
  by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
  · rw [← hA] at h'x
    obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
      simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
    right
    exact mem_biUnion pA ⟨hx, xp⟩
  · exact Or.inl ⟨hx, h'x⟩
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
⊢ s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
intro x hx
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
[GOAL]
case pos
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
rw [← hA] at h'x
[GOAL]
case pos
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
  simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ ∃ p, p ∈ A ∧ x ∈ T p
[PROOFSTEP]
simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
[GOAL]
case pos.intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
right
[GOAL]
case pos.intro.intro.h
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
exact mem_biUnion pA ⟨hx, xp⟩
[GOAL]
case neg
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : ¬x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
[PROOFSTEP]
exact Or.inl ⟨hx, h'x⟩
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
[PROOFSTEP]
apply ae_restrict_of_ae_restrict_of_subset this
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p), p x
[PROOFSTEP]
rw [ae_restrict_union_iff, ae_restrict_biUnion_iff _ A_count]
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ (∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x) ∧ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T i), p x
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.left
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x
[PROOFSTEP]
have : μ.restrict (s \ u) = 0 := by simp only [restrict_eq_zero, hfinite.measure_zero]
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ Measure.restrict μ (s \ u) = 0
[PROOFSTEP]
simp only [restrict_eq_zero, hfinite.measure_zero]
[GOAL]
case intro.intro.left
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this✝ : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
this : Measure.restrict μ (s \ u) = 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x
[PROOFSTEP]
simp only [this, ae_zero, eventually_bot]
[GOAL]
case intro.intro.right
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T i), p x
[PROOFSTEP]
rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
[GOAL]
case intro.intro.right.mk.mk.mk
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T ({ val := a, property := as }, { val := b, property := bs })), p x
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.right.mk.mk.mk
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
[PROOFSTEP]
rcases le_or_lt b a with (hba | hab)
[GOAL]
case intro.intro.right.mk.mk.mk.inl
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
[PROOFSTEP]
simp only [Ioo_eq_empty_of_le hba, inter_empty, restrict_empty, ae_zero, eventually_bot]
[GOAL]
case intro.intro.right.mk.mk.mk.inr
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
[PROOFSTEP]
exact h a b as bs hab
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
let T : s × s → Set ℝ := fun p => Ioo p.1 p.2
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
let u := ⋃ i : ↥s × ↥s, T i
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
obtain ⟨A, A_count, hA⟩ : ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
  isOpen_iUnion_countable _ fun p => isOpen_Ioo
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
have M : ∀ᵐ x ∂μ, x ∉ s \ u := hfinite.countable.ae_not_mem _
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
have M' : ∀ᵐ x ∂μ, ∀ (i : ↥s × ↥s), i ∈ A → x ∈ s ∩ T i → p x :=
  by
  rw [ae_ball_iff A_count]
  rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
  change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
  rcases le_or_lt b a with (hba | hab)
  · simp only [Ioo_eq_empty_of_le hba, inter_empty, IsEmpty.forall_iff, eventually_true, mem_empty_iff_false]
  · exact h a b as bs hab
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
⊢ ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
[PROOFSTEP]
rw [ae_ball_iff A_count]
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
⊢ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ T i → p x
[PROOFSTEP]
rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
[GOAL]
case mk.mk.mk
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ T ({ val := a, property := as }, { val := b, property := bs }) → p x
[PROOFSTEP]
change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
[GOAL]
case mk.mk.mk
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
[PROOFSTEP]
rcases le_or_lt b a with (hba | hab)
[GOAL]
case mk.mk.mk.inl
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
[PROOFSTEP]
simp only [Ioo_eq_empty_of_le hba, inter_empty, IsEmpty.forall_iff, eventually_true, mem_empty_iff_false]
[GOAL]
case mk.mk.mk.inr
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
[PROOFSTEP]
exact h a b as bs hab
[GOAL]
case intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
[PROOFSTEP]
filter_upwards [M, M'] with x hx h'x
[GOAL]
case h
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p x
⊢ x ∈ s → p x
[PROOFSTEP]
intro xs
[GOAL]
case h
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p x
xs : x ∈ s
⊢ p x
[PROOFSTEP]
by_cases Hx : x ∈ ⋃ i : ↥s × ↥s, T i
[GOAL]
case pos
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p x
xs : x ∈ s
Hx : x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ p x
[PROOFSTEP]
rw [← hA] at Hx
[GOAL]
case pos
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p x
xs : x ∈ s
Hx : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ p x
[PROOFSTEP]
obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
  simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx
[GOAL]
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p x
xs : x ∈ s
Hx : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ ∃ p, p ∈ A ∧ x ∈ T p
[PROOFSTEP]
simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx
[GOAL]
case pos.intro.intro
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p✝ x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p✝ x
xs : x ∈ s
Hx : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ p✝ x
[PROOFSTEP]
apply h'x p pA ⟨xs, xp⟩
[GOAL]
case neg
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i = ⋃ (i : ↑s × ↑s), T i
M : ∀ᵐ (x : ℝ) ∂μ, ¬x ∈ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ T i → p x
x : ℝ
hx : ¬x ∈ s \ ⋃ (i : ↑s × ↑s), Ioo ↑i.fst ↑i.snd
h'x : ∀ (i : ↑s × ↑s), i ∈ A → x ∈ s ∩ Ioo ↑i.fst ↑i.snd → p x
xs : x ∈ s
Hx : ¬x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ p x
[PROOFSTEP]
exact False.elim (hx ⟨xs, Hx⟩)