α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ
haveI : Fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
h_comp :
  (fun f => ∫ (x : α) in s, ↑↑f x ∂μ) =
    integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ
have h_comp :
  (fun f : α →₁[μ] E => ∫ x in s, f x ∂μ) =
    integral (μ.restrict s) ∘ fun f => LpToLpRestrictCLM α E ℝ μ 1 s f := by
  ext1 f
  rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
h_comp :
  (fun f => ∫ (x : α) in s, ↑↑f x ∂μ) =
    integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)
⊢ Continuous (integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f))
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
h_comp :
  (fun f => ∫ (x : α) in s, ↑↑f x ∂μ) =
    integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ
rw [h_comp]
no goals
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
h_comp :
  (fun f => ∫ (x : α) in s, ↑↑f x ∂μ) =
    integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)
⊢ Continuous (integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f))
exact continuous_integral.comp (LpToLpRestrictCLM α E ℝ μ 1 s).continuous
case h
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
f : { x // x ∈ Lp E 1 }
⊢ (∫ (x : α) in s, ↑↑f x ∂μ) = (integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)) f
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
⊢ (fun f => ∫ (x : α) in s, ↑↑f x ∂μ) =
    integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)
ext1 f
no goals
case h
α : Type u_2
β : Type ?u.347428
E : Type u_1
F : Type ?u.347434
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type ?u.347443
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
this : Fact (1 ≤ 1)
f : { x // x ∈ Lp E 1 }
⊢ (∫ (x : α) in s, ↑↑f x ∂μ) = (integral (Measure.restrict μ s) ∘ fun f => ↑↑(↑(LpToLpRestrictCLM α E ℝ μ 1 s) f)) f
rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]