α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ((∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ inner (indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
rw [inner_def, ← integral_add_compl hs (L2.integrable_inner _ f)]
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ((∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ((∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
have h_left : (∫ x in s, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = ∫ x in s, ⟪c, f x⟫ ∂μ := by
  suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫
  exact set_integral_congr_ae hs h_ae_eq
  have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c :=
    indicatorConstLp_coeFn_mem
  refine' h_indicator.mono fun x hx hxs => _
  congr
  exact hx hxs
no goals
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_right : (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0
⊢ ((∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
rw [h_left, h_right, add_zero]
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
⊢ (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ

case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
⊢ (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ

case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
exact set_integral_congr_ae hs h_ae_eq
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c :=
  indicatorConstLp_coeFn_mem
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
refine' h_indicator.mono fun x hx hxs => _
case h_ae_eq.e_a
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ ↑↑(indicatorConstLp 2 hs hμs c) x = c
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
congr
no goals
case h_ae_eq.e_a
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ ↑↑(indicatorConstLp 2 hs hμs c) x = c
exact hx hxs
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0

case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 :=
  indicatorConstLp_coeFn_nmem
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : ¬x ∈ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
refine' h_indicator.mono fun x hx hxs => _
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : ¬x ∈ s
⊢ inner 0 (↑↑f x) = 0
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : ¬x ∈ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
rw [hx hxs]
no goals
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : ¬x ∈ s
⊢ inner 0 (↑↑f x) = 0
exact inner_zero_left _
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0
simp_rw [← Set.mem_compl_iff] at h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0

case h_int_zero
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in sᶜ, 0 ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0
suffices h_int_zero :
  (∫ x in sᶜ, inner (indicatorConstLp 2 hs hμs c x) (f x) ∂μ) = ∫ _ in sᶜ, (0 : 𝕜) ∂μ
no goals
case h_int_zero
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in sᶜ, 0 ∂μ
exact set_integral_congr_ae hs.compl h_ae_eq
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ (∫ (x : α) in sᶜ, 0 ∂μ) = 0
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = 0
rw [h_int_zero]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.150378
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : (∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : (∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ) = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ (∫ (x : α) in sᶜ, 0 ∂μ) = 0
simp