Theorem: average_linear_comm (Ray/Misc/Measure.lean)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
⊢ ⨍ (x : X) in s, g (f x) = g (⨍ (x : X) in s, f x)
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  LinearMapClass.map_smul]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Tactic:
by_cases v0 : (volume s).toReal = 0
State after:
case pos
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : (↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

case neg
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

State before:
case pos
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : (↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

case neg
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Tactic:
simp [v0]
State after:
case neg
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

State before:
case neg
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Tactic:
rw [(Ne.isUnit v0).inv.smul_left_cancel]
State after:
case neg
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ ∫ (x : X) in s, g (f x) = g (∫ (x : X) in s, f x)

State before:
case neg
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ ∫ (x : X) in s, g (f x) = g (∫ (x : X) in s, f x)
Tactic:
exact ContinuousLinearMap.integral_comp_comm _ fi
State after:
no goals