case pos
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : Integrable φ
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)

case neg
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)
by_cases h : Integrable φ μ
case neg
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
this : ¬Integrable fun a => ↑L (φ a)
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)
case neg
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)
have : ¬Integrable (fun a => L (φ a)) μ := by
  erw [LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]
  assumption
no goals
case neg
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
this : ¬Integrable fun a => ↑L (φ a)
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)
simp [integral_undef, h, this]
no goals
case pos
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : Integrable φ
⊢ (∫ (a : α), ↑L (φ a) ∂μ) = ↑L (∫ (a : α), φ a ∂μ)
exact integral_comp_comm L h
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
⊢ ¬Integrable fun a => φ a
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
⊢ ¬Integrable fun a => ↑L (φ a)
erw [LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]
no goals
α : Type u_4
β : Type ?u.1835818
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
ι : Type ?u.1835830
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
L : E →L[𝕜] F
K : ℝ≥0
hL : AntilipschitzWith K ↑L
φ : α → E
h : ¬Integrable φ
⊢ ¬Integrable fun a => φ a
assumption