α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 0)
refine' Metric.tendsto_nhds.2 fun ε εpos => _
case intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
⊢ ∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
obtain ⟨δ, hδ, δpos⟩ : ∃ δ, (δ * ∫ x in s, ‖g x‖ ∂μ) + δ < ε ∧ 0 < δ := by
  have A :
    Tendsto (fun δ => (δ * ∫ x in s, ‖g x‖ ∂μ) + δ) (𝓝[>] 0)
      (𝓝 ((0 * ∫ x in s, ‖g x‖ ∂μ) + 0)) := by
    apply Tendsto.mono_left _ nhdsWithin_le_nhds
    exact (tendsto_id.mul tendsto_const_nhds).add tendsto_id
  rw [MulZeroClass.zero_mul, zero_add] at A
  exact (((tendsto_order.1 A).2 ε εpos).and self_mem_nhdsWithin).exists
case intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
⊢ ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
case intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
⊢ ∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
suffices ∀ᶠ i in l, ‖∫ x in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ x in s, ‖g x‖ ∂μ) + δ by
  filter_upwards [this] with i hi
  simp only [dist_zero_right]
  exact hi.trans_lt hδ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
⊢ ∃ u, IsOpen u ∧ x₀ ∈ u ∧ ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ

case intro.intro.intro.intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
⊢ ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
case intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
⊢ ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
obtain ⟨u, u_open, x₀u, hu⟩ : ∃ u, IsOpen u ∧ x₀ ∈ u ∧ ∀ x ∈ u ∩ s, g x ∈ ball (g x₀) δ
case intro.intro.intro.intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
⊢ ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
⊢ ∃ u, IsOpen u ∧ x₀ ∈ u ∧ ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ

case intro.intro.intro.intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
⊢ ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
exact mem_nhdsWithin.1 (hcg (ball_mem_nhds _ δpos))
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
case intro.intro.intro.intro.intro
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
⊢ ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
filter_upwards [tendstoUniformlyOn_iff.1 (hlφ u u_open x₀u) δ δpos, hiφ, hnφ,
  integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt hs hlφ hiφ hmg hcg] with i hi h'i
  hφpos h''i
no goals
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
C : ‖∫ (x : α) in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
calc
  ‖∫ x in s, φ i x • g x ∂μ‖ =
    ‖(∫ x in s \ u, φ i x • g x ∂μ) + ∫ x in s ∩ u, φ i x • g x ∂μ‖ := by
    conv_lhs => rw [← diff_union_inter s u]
    rw [integral_union (disjoint_sdiff_inter _ _) (hs.inter u_open.measurableSet)
        (h''i.mono_set (diff_subset _ _)) (h''i.mono_set (inter_subset_left _ _))]
  _ ≤ ‖∫ x in s \ u, φ i x • g x ∂μ‖ + ‖∫ x in s ∩ u, φ i x • g x ∂μ‖ := (norm_add_le _ _)
  _ ≤ (δ * ∫ x in s, ‖g x‖ ∂μ) + δ := add_le_add C B
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
A : Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝[Ioi 0] 0) (𝓝 ((0 * ∫ (x : α) in s, ‖g x‖ ∂μ) + 0))
⊢ ∃ δ, (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε ∧ 0 < δ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
⊢ ∃ δ, (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε ∧ 0 < δ
have A :
  Tendsto (fun δ => (δ * ∫ x in s, ‖g x‖ ∂μ) + δ) (𝓝[>] 0)
    (𝓝 ((0 * ∫ x in s, ‖g x‖ ∂μ) + 0)) := by
  apply Tendsto.mono_left _ nhdsWithin_le_nhds
  exact (tendsto_id.mul tendsto_const_nhds).add tendsto_id
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
A : Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ ∃ δ, (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε ∧ 0 < δ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
A : Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝[Ioi 0] 0) (𝓝 ((0 * ∫ (x : α) in s, ‖g x‖ ∂μ) + 0))
⊢ ∃ δ, (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε ∧ 0 < δ
rw [MulZeroClass.zero_mul, zero_add] at A
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
A : Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ ∃ δ, (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε ∧ 0 < δ
exact (((tendsto_order.1 A).2 ε εpos).and self_mem_nhdsWithin).exists
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
⊢ Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝 0) (𝓝 ((0 * ∫ (x : α) in s, ‖g x‖ ∂μ) + 0))
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
⊢ Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝[Ioi 0] 0) (𝓝 ((0 * ∫ (x : α) in s, ‖g x‖ ∂μ) + 0))
apply Tendsto.mono_left _ nhdsWithin_le_nhds
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
⊢ Tendsto (fun δ => (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ) (𝓝 0) (𝓝 ((0 * ∫ (x : α) in s, ‖g x‖ ∂μ) + 0))
exact (tendsto_id.mul tendsto_const_nhds).add tendsto_id
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
i : ι
hi : ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
⊢ dist (∫ (x : α) in s, φ i x • g x ∂μ) 0 < ε
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
⊢ ∀ᶠ (x : ι) in l, dist (∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ) 0 < ε
filter_upwards [this] with i hi
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
i : ι
hi : ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
⊢ ‖∫ (x : α) in s, φ i x • g x ∂μ‖ < ε
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
i : ι
hi : ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
⊢ dist (∫ (x : α) in s, φ i x • g x ∂μ) 0 < ε
simp only [dist_zero_right]
no goals
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
this : ∀ᶠ (i : ι) in l, ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
i : ι
hi : ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ
⊢ ‖∫ (x : α) in s, φ i x • g x ∂μ‖ < ε
exact hi.trans_lt hδ
case refine'_1
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ IntegrableOn (fun x => ‖φ i x • g x‖) (s ∩ u)

case refine'_2
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ IntegrableOn (fun x => ‖φ i x‖ * δ) (s ∩ u)

case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖φ i x • g x‖ ≤ ‖φ i x‖ * δ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ (∫ (x : α) in s ∩ u, ‖φ i x • g x‖ ∂μ) ≤ ∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ
refine' set_integral_mono_on _ _ (hs.inter u_open.measurableSet) fun x hx => _
case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖φ i x‖ * ‖g x‖ ≤ ‖φ i x‖ * δ
case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖φ i x • g x‖ ≤ ‖φ i x‖ * δ
rw [norm_smul]
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ δ
case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖φ i x‖ * ‖g x‖ ≤ ‖φ i x‖ * δ
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ s ∩ u → g x ∈ ball 0 δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ δ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ δ
rw [inter_comm, h'g] at hu
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ s ∩ u → g x ∈ ball 0 δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ δ
exact (mem_ball_zero_iff.1 (hu x hx)).le
no goals
case refine'_1
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ IntegrableOn (fun x => ‖φ i x • g x‖) (s ∩ u)
exact IntegrableOn.mono_set h''i.norm (inter_subset_left _ _)
no goals
case refine'_2
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ IntegrableOn (fun x => ‖φ i x‖ * δ) (s ∩ u)
exact
  IntegrableOn.mono_set ((integrable_of_integral_eq_one h'i).norm.mul_const _)
    (inter_subset_left _ _)
case hfi
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ IntegrableOn (fun x => ‖φ i x‖ * δ) s

case hf
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ 0 ≤ᶠ[ae (Measure.restrict μ s)] fun x => ‖φ i x‖ * δ

case hst
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ s ∩ u ≤ᶠ[ae μ] s
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ (∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ) ≤ ∫ (x : α) in s, ‖φ i x‖ * δ ∂μ
apply set_integral_mono_set
no goals
case hfi
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ IntegrableOn (fun x => ‖φ i x‖ * δ) s
exact (integrable_of_integral_eq_one h'i).norm.mul_const _
no goals
case hf
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ 0 ≤ᶠ[ae (Measure.restrict μ s)] fun x => ‖φ i x‖ * δ
exact eventually_of_forall fun x => mul_nonneg (norm_nonneg _) δpos.le
case hst.hp
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ ∀ (x : α), (s ∩ u) x ≤ s x
case hst
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ s ∩ u ≤ᶠ[ae μ] s
apply eventually_of_forall
no goals
case hst.hp
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ ∀ (x : α), (s ∩ u) x ≤ s x
exact inter_subset_left s u
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s
⊢ ‖φ i x‖ * δ = φ i x * δ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ (∫ (x : α) in s, ‖φ i x‖ * δ ∂μ) = ∫ (x : α) in s, φ i x * δ ∂μ
apply set_integral_congr hs fun x hx => ?_
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
x : α
hx : x ∈ s
⊢ ‖φ i x‖ * δ = φ i x * δ
rw [Real.norm_of_nonneg (hφpos _ hx)]
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
⊢ (∫ (x : α) in s, φ i x * δ ∂μ) = δ
rw [integral_mul_right, h'i, one_mul]
case refine'_1
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ IntegrableOn (fun x => ‖φ i x • g x‖) (s \ u)

case refine'_2
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ IntegrableOn (fun x => δ * ‖g x‖) (s \ u)

case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x • g x‖ ≤ δ * ‖g x‖
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ (∫ (x : α) in s \ u, ‖φ i x • g x‖ ∂μ) ≤ ∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ
refine' set_integral_mono_on _ _ (hs.diff u_open.measurableSet) fun x hx => _
case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ * ‖g x‖ ≤ δ * ‖g x‖
case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x • g x‖ ≤ δ * ‖g x‖
rw [norm_smul]
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ δ
case refine'_3
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ * ‖g x‖ ≤ δ * ‖g x‖
apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ δ
simpa only [Pi.zero_apply, dist_zero_left] using (hi x hx).le
no goals
case refine'_1
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ IntegrableOn (fun x => ‖φ i x • g x‖) (s \ u)
exact IntegrableOn.mono_set h''i.norm (diff_subset _ _)
no goals
case refine'_2
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ IntegrableOn (fun x => δ * ‖g x‖) (s \ u)
exact IntegrableOn.mono_set (hmg.norm.const_mul _) (diff_subset _ _)
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ (δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ (∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
rw [integral_mul_left]
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ 0 ≤ᶠ[ae (Measure.restrict μ s)] fun a => ‖g a‖

α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ s \ u ≤ᶠ[ae μ] s
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ (δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
apply mul_le_mul_of_nonneg_left (set_integral_mono_set hmg.norm _ _) δpos.le
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ 0 ≤ᶠ[ae (Measure.restrict μ s)] fun a => ‖g a‖
exact eventually_of_forall fun x => norm_nonneg _
case hp
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ ∀ (x : α), (s \ u) x ≤ s x
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ s \ u ≤ᶠ[ae μ] s
apply eventually_of_forall
no goals
case hp
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
⊢ ∀ (x : α), (s \ u) x ≤ s x
exact diff_subset s u
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
C : ‖∫ (x : α) in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ‖∫ (x : α) in s \ u ∪ s ∩ u, φ i x • g x ∂μ‖ =
    ‖(∫ (x : α) in s \ u, φ i x • g x ∂μ) + ∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
C : ‖∫ (x : α) in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ‖∫ (x : α) in s, φ i x • g x ∂μ‖ = ‖(∫ (x : α) in s \ u, φ i x • g x ∂μ) + ∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖
conv_lhs => rw [← diff_union_inter s u]
no goals
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : ∀ᶠ (i : ι) in l, (∫ (x : α) in s, φ i x ∂μ) = 1
hmg : IntegrableOn g s
h'g : g x₀ = 0
hcg : ContinuousWithinAt g s x₀
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : (δ * ∫ (x : α) in s, ‖g x‖ ∂μ) + δ < ε
δpos : 0 < δ
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
hu : ∀ (x : α), x ∈ u ∩ s → g x ∈ ball (g x₀) δ
i : ι
hi : ∀ (x : α), x ∈ s \ u → dist (OfNat.ofNat 0 x) (φ i x) < δ
h'i : (∫ (x : α) in s, φ i x ∂μ) = 1
hφpos : ∀ (x : α), x ∈ s → 0 ≤ φ i x
h''i : IntegrableOn (fun x => φ i x • g x) s
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ δ
C : ‖∫ (x : α) in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ‖∫ (x : α) in s \ u ∪ s ∩ u, φ i x • g x ∂μ‖ =
    ‖(∫ (x : α) in s \ u, φ i x • g x ∂μ) + ∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖
rw [integral_union (disjoint_sdiff_inter _ _) (hs.inter u_open.measurableSet)
    (h''i.mono_set (diff_subset _ _)) (h''i.mono_set (inter_subset_left _ _))]