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 (abs (det (Matrix.diagonal D))⁻¹) • volume

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 (abs (det (TransvectionStruct.toMatrix t))⁻¹) • volume

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 (abs (det A)⁻¹) • volume →
          Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume →
            Measure.map (↑(↑toLin' (A ⬝ B))) volume = ofReal (abs (det (A ⬝ B))⁻¹) • volume
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : det M ≠ 0
⊢ Measure.map (↑(↑toLin' M)) volume = ofReal (abs (det M)⁻¹) • volume
apply diagonal_transvection_induction_of_det_ne_zero _ M hM
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 (abs (det (Matrix.diagonal D))⁻¹) • volume
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 (abs (det (Matrix.diagonal D))⁻¹) • volume
intro D hD
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 (abs (det (Matrix.diagonal D))⁻¹) •
      ofReal (abs (det (Matrix.diagonal D))) • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume
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 (abs (det (Matrix.diagonal D))⁻¹) • volume
conv_rhs => rw [← smul_map_diagonal_volume_pi hD]
no goals
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 (abs (det (Matrix.diagonal D))⁻¹) •
      ofReal (abs (det (Matrix.diagonal D))) • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume
rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel hD, abs_one,
  ENNReal.ofReal_one, one_smul]
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 (abs (det (TransvectionStruct.toMatrix t))⁻¹) • volume
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 (abs (det (TransvectionStruct.toMatrix t))⁻¹) • volume
intro t
no goals
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 (abs (det (TransvectionStruct.toMatrix t))⁻¹) • volume
simp only [Matrix.TransvectionStruct.det, ENNReal.ofReal_one,
  (volume_preserving_transvectionStruct _).map_eq, one_smul, _root_.inv_one, abs_one]
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Measure.map (↑(↑toLin' (A ⬝ B))) volume = ofReal (abs (det (A ⬝ B))⁻¹) • volume
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 (abs (det A)⁻¹) • volume →
          Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume →
            Measure.map (↑(↑toLin' (A ⬝ B))) volume = ofReal (abs (det (A ⬝ B))⁻¹) • volume
intro A B _ _ IHA IHB
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Measurable ↑(↑toLin' A)

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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Measurable ↑(↑toLin' B)
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Measure.map (↑(↑toLin' (A ⬝ B))) volume = ofReal (abs (det (A ⬝ B))⁻¹) • volume
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]
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Continuous ↑(↑toLin' A)
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Measurable ↑(↑toLin' A)
apply Continuous.measurable
no goals
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Continuous ↑(↑toLin' A)
apply LinearMap.continuous_on_pi
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Continuous ↑(↑toLin' B)
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Measurable ↑(↑toLin' B)
apply Continuous.measurable
no goals
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 (abs (det A)⁻¹) • volume
IHB : Measure.map (↑(↑toLin' B)) volume = ofReal (abs (det B)⁻¹) • volume
⊢ Continuous ↑(↑toLin' B)
apply LinearMap.continuous_on_pi