α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∃ u,
    Monotone u ∧
      Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
have h :=
  @exists_seq_tendsto_sSup _ _ _ _ _ (measurableLEEval ν μ)
    ⟨0, 0, zero_mem_measurableLE, by simp⟩ (OrderTop.bddAbove _)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∃ u,
    Monotone u ∧
      Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
choose g _ hg₂ f hf₁ hf₂ using h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
set ξ := ⨆ (n) (k) (hk : k ≤ n), f k with hξ
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
have hξm : Measurable ξ := by
  convert measurable_iSup fun n => (iSup_mem_measurableLE _ hf₁ n).1
  refine Option.ext fun x => ?_; simp [hξ]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
set μ₁ := μ - ν.withDensity ξ with hμ₁
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
have hle : ν.withDensity ξ ≤ μ := by
  intro B hB
  rw [hξ, withDensity_apply _ hB]
  simp_rw [iSup_apply]
  rw [lintegral_iSup (fun i => (iSup_mem_measurableLE _ hf₁ i).1) (iSup_monotone _)]
  exact iSup_le fun i => (iSup_mem_measurableLE _ hf₁ i).2 B hB
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
have : IsFiniteMeasure (ν.withDensity ξ) := by
  refine' isFiniteMeasure_withDensity _
  have hle' := hle univ MeasurableSet.univ
  rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at hle'
  exact ne_top_of_le_ne_top (measure_ne_top _ _) hle'
case refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ (μ₁, ξ).fst ⟂ₘ ν

case refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ μ = (μ₁, ξ).fst + withDensity ν (μ₁, ξ).snd
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd
refine' ⟨⟨μ₁, ξ⟩, hξm, _, _⟩
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (fun f => ∫⁻ (x : α), f x ∂ν) 0 = 0
simp
case refine_4
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν

case refine_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∀ (n : ℕ), AEMeasurable ((fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n)

case refine_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∀ᵐ (x : α) ∂ν, Monotone fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x

case refine_3
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x) Filter.atTop
      (nhds (iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x))
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
have :=
  @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n => ⨆ (k) (_ : k ≤ n), f k)
    (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
case refine_4
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (sSup (measurableLEEval ν μ)))
case refine_4
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
refine' tendsto_nhds_unique _ this
case refine_4.refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ g ≤ fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν

case refine_4.refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) ≤ fun x => sSup (measurableLEEval ν μ)
case refine_4
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (sSup (measurableLEEval ν μ)))
refine' tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds _ _
case refine_4.refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ g n ≤ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) n
case refine_4.refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ g ≤ fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν
intro n
case refine_4.refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ (fun f => ∫⁻ (x : α), f x ∂ν) (f n) ≤ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) n
case refine_4.refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ g n ≤ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) n
rw [← hf₂ n]
case refine_4.refine'_1.hfg
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ (fun a => f n a) ≤ fun a => iSup (fun k => ⨆ (_ : k ≤ n), f k) a
case refine_4.refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ (fun f => ∫⁻ (x : α), f x ∂ν) (f n) ≤ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) n
apply lintegral_mono
no goals
case refine_4.refine'_1.hfg
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ (fun a => f n a) ≤ fun a => iSup (fun k => ⨆ (_ : k ≤ n), f k) a
simp only [iSup_apply, iSup_le_le f n n le_rfl]
case refine_4.refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) n ≤ (fun x => sSup (measurableLEEval ν μ)) n
case refine_4.refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
⊢ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) ≤ fun x => sSup (measurableLEEval ν μ)
intro n
no goals
case refine_4.refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ (fun n => ∫⁻ (x : α), iSup (fun k => ⨆ (_ : k ≤ n), f k) x ∂ν) n ≤ (fun x => sSup (measurableLEEval ν μ)) n
exact le_sSup ⟨⨆ (k : ℕ) (_ : k ≤ n), f k, iSup_mem_measurableLE' _ hf₁ _, rfl⟩
case refine_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
⊢ AEMeasurable ((fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n)
case refine_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∀ (n : ℕ), AEMeasurable ((fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n)
intro n
case refine_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
⊢ Measurable ((fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n)
case refine_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
⊢ AEMeasurable ((fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n)
refine' Measurable.aemeasurable _
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
x✝ : α
⊢ (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x✝ = ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
case refine_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
⊢ Measurable ((fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n)
convert (iSup_mem_measurableLE _ hf₁ n).1
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
x✝ : α
x : ℝ≥0
⊢ x ∈ (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x✝ ↔ x ∈ ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
x✝ : α
⊢ (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x✝ = ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
refine Option.ext fun x => ?_
no goals
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
n : ℕ
x✝ : α
x : ℝ≥0
⊢ x ∈ (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x✝ ↔ x ∈ ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
simp
case refine_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
a : α
⊢ Monotone fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n a
case refine_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∀ᵐ (x : α) ∂ν, Monotone fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x
refine' Filter.eventually_of_forall fun a => _
no goals
case refine_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
a : α
⊢ Monotone fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n a
simp [iSup_monotone' f _]
case refine_3
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
a : α
⊢ Filter.Tendsto (fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n a) Filter.atTop
    (nhds (iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a))
case refine_3
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
⊢ ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n x) Filter.atTop
      (nhds (iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) x))
refine' Filter.eventually_of_forall fun a => _
no goals
case refine_3
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
a : α
⊢ Filter.Tendsto (fun n => (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) n a) Filter.atTop
    (nhds (iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a))
simp [tendsto_atTop_iSup (iSup_monotone' f a)]
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
x✝ : α
⊢ ξ x✝ = ⨆ (i : ℕ) (k : ℕ) (_ : k ≤ i), f k x✝
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
⊢ Measurable ξ
convert measurable_iSup fun n => (iSup_mem_measurableLE _ hf₁ n).1
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
x✝ : α
x : ℝ≥0
⊢ x ∈ ξ x✝ ↔ x ∈ ⨆ (i : ℕ) (k : ℕ) (_ : k ≤ i), f k x✝
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
x✝ : α
⊢ ξ x✝ = ⨆ (i : ℕ) (k : ℕ) (_ : k ≤ i), f k x✝
refine Option.ext fun x => ?_
no goals
case h.e'_5.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
x✝ : α
x : ℝ≥0
⊢ x ∈ ξ x✝ ↔ x ∈ ⨆ (i : ℕ) (k : ℕ) (_ : k ≤ i), f k x✝
simp [hξ]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ ↑↑(withDensity ν ξ) B ≤ ↑↑μ B
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
⊢ withDensity ν ξ ≤ μ
intro B hB
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ (∫⁻ (a : α) in B, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν) ≤ ↑↑μ B
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ ↑↑(withDensity ν ξ) B ≤ ↑↑μ B
rw [hξ, withDensity_apply _ hB]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ (∫⁻ (a : α) in B, ⨆ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), f i_1 a ∂ν) ≤ ↑↑μ B
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ (∫⁻ (a : α) in B, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν) ≤ ↑↑μ B
simp_rw [iSup_apply]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ (⨆ (n : ℕ), ∫⁻ (a : α) in B, ⨆ (k : ℕ) (_ : k ≤ n), f k a ∂ν) ≤ ↑↑μ B
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ (∫⁻ (a : α) in B, ⨆ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), f i_1 a ∂ν) ≤ ↑↑μ B
rw [lintegral_iSup (fun i => (iSup_mem_measurableLE _ hf₁ i).1) (iSup_monotone _)]
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
B : Set α
hB : MeasurableSet B
⊢ (⨆ (n : ℕ), ∫⁻ (a : α) in B, ⨆ (k : ℕ) (_ : k ≤ n), f k a ∂ν) ≤ ↑↑μ B
exact iSup_le fun i => (iSup_mem_measurableLE _ hf₁ i).2 B hB
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
⊢ IsFiniteMeasure (withDensity ν ξ)
refine' isFiniteMeasure_withDensity _
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
hle' : ↑↑(withDensity ν ξ) univ ≤ ↑↑μ univ
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
have hle' := hle univ MeasurableSet.univ
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
hle' : (∫⁻ (a : α), ξ a ∂ν) ≤ ↑↑μ univ
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
hle' : ↑↑(withDensity ν ξ) univ ≤ ↑↑μ univ
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at hle'
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
hle' : (∫⁻ (a : α), ξ a ∂ν) ≤ ↑↑μ univ
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
exact ne_top_of_le_ne_top (measure_ne_top _ _) hle'
case refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
⊢ False
case refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ (μ₁, ξ).fst ⟂ₘ ν
by_contra h
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ : VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (toSignedMeasure μ₁ - toSignedMeasure (ε • ν)) E
⊢ False
case refine'_1
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
⊢ False
obtain ⟨ε, hε₁, E, hE₁, hE₂, hE₃⟩ := exists_positive_of_not_mutuallySingular μ₁ ν h
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
⊢ False
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ : VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (toSignedMeasure μ₁ - toSignedMeasure (ε • ν)) E
⊢ False
simp_rw [hμ₁] at hE₃
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
⊢ False
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
⊢ False
have hξle : ∀ A, MeasurableSet A → (∫⁻ a in A, ξ a ∂ν) ≤ μ A := by
  intro A hA; rw [hξ]
  simp_rw [iSup_apply]
  rw [lintegral_iSup (fun n => (iSup_mem_measurableLE _ hf₁ n).1) (iSup_monotone _)]
  exact iSup_le fun n => (iSup_mem_measurableLE _ hf₁ n).2 A hA
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
⊢ False
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
⊢ False
have hξε : (ξ + E.indicator fun _ => (ε : ℝ≥0∞)) ∈ measurableLE ν μ := by
  refine' ⟨Measurable.add hξm (Measurable.indicator measurable_const hE₁), fun A hA => _⟩
  have :
    (∫⁻ a in A, (ξ + E.indicator fun _ => (ε : ℝ≥0∞)) a ∂ν) =
      (∫⁻ a in A ∩ E, ε + ξ a ∂ν) + ∫⁻ a in A \ E, ξ a ∂ν := by
    simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
      set_lintegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, Pi.add_apply,
      lintegral_indicator _ hE₁, restrict_apply hE₁]
    rw [inter_comm, add_comm]
  rw [this, ← measure_inter_add_diff A hE₁]
  exact add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁))
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ False
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
⊢ False
have : (∫⁻ a, ξ a + E.indicator (fun _ => (ε : ℝ≥0∞)) a ∂ν) ≤ sSup (measurableLEEval ν μ) :=
  le_sSup ⟨ξ + E.indicator fun _ => (ε : ℝ≥0∞), hξε, rfl⟩
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ sSup (measurableLEEval ν μ) < ∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ False
refine' not_lt.2 this _
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ (∫⁻ (a : α), ξ a ∂ν) < (∫⁻ (a : α), ξ a ∂ν) + ↑ε * ↑↑ν E
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ sSup (measurableLEEval ν μ) < ∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν
rw [hξ₁, lintegral_add_left hξm, lintegral_indicator _ hE₁, set_lintegral_const]
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ (∫⁻ (a : α), ξ a ∂ν) < (∫⁻ (a : α), ξ a ∂ν) + ↑ε * ↑↑ν E
refine' ENNReal.lt_add_right _ (ENNReal.mul_pos_iff.2 ⟨ENNReal.coe_pos.2 hε₁, hE₂⟩).ne'
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝¹ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this✝ : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
this : ↑↑(withDensity ν ξ) univ ≠ ⊤
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
have := measure_ne_top (ν.withDensity ξ) univ
no goals
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝¹ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
hξε : (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
this✝ : (∫⁻ (a : α), ξ a + indicator E (fun x => ↑ε) a ∂ν) ≤ sSup (measurableLEEval ν μ)
this : ↑↑(withDensity ν ξ) univ ≠ ⊤
⊢ (∫⁻ (a : α), ξ a ∂ν) ≠ ⊤
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at this
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
⊢ ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
intro A hA
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
rw [hξ]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, ⨆ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), f i_1 a ∂ν) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν) ≤ ↑↑μ A
simp_rw [iSup_apply]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (⨆ (n : ℕ), ∫⁻ (a : α) in A, ⨆ (k : ℕ) (_ : k ≤ n), f k a ∂ν) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, ⨆ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), f i_1 a ∂ν) ≤ ↑↑μ A
rw [lintegral_iSup (fun n => (iSup_mem_measurableLE _ hf₁ n).1) (iSup_monotone _)]
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
A : Set α
hA : MeasurableSet A
⊢ (⨆ (n : ℕ), ∫⁻ (a : α) in A, ⨆ (k : ℕ) (_ : k ≤ n), f k a ∂ν) ≤ ↑↑μ A
exact iSup_le fun n => (iSup_mem_measurableLE _ hf₁ n).2 A hA
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
⊢ ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
intro A hA
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ↑0 (A ∩ E) ≤ ↑(toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) (A ∩ E)
⊢ (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
have := subset_le_of_restrict_le_restrict _ _ hE₁ hE₃ (inter_subset_right A E)
case ha
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E) ≠ ⊤

case hb
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑μ (A ∩ E) ≠ ⊤

case ha
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E)) + ENNReal.toReal (↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑(ε • ν) (A ∩ E) ≠ ⊤

case hb
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E)) + ENNReal.toReal (↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑(withDensity ν ξ) (A ∩ E) ≠ ⊤

α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : 0 ≤ ENNReal.toReal (↑↑μ (A ∩ E) - ↑↑(withDensity ν ξ) (A ∩ E)) - ENNReal.toReal (↑↑(ε • ν) (A ∩ E))
⊢ ↑↑(withDensity ν ξ) (A ∩ E) ≤ ↑↑μ (A ∩ E)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ↑0 (A ∩ E) ≤ ↑(toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) (A ∩ E)
⊢ (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
rwa [zero_apply, toSignedMeasure_sub_apply (hA.inter hE₁),
  Measure.sub_apply (hA.inter hE₁) hle,
  ENNReal.toReal_sub_of_le _ (ne_of_lt (measure_lt_top _ _)), sub_nonneg, le_sub_iff_add_le,
  ← ENNReal.toReal_add, ENNReal.toReal_le_toReal, Measure.coe_smul, Pi.smul_apply,
  withDensity_apply _ (hA.inter hE₁), show ε • ν (A ∩ E) = (ε : ℝ≥0∞) * ν (A ∩ E) by rfl,
  ← set_lintegral_const, ← lintegral_add_left measurable_const] at this
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : (ε • ↑↑ν (A ∩ E) + ∫⁻ (a : α) in A ∩ E, ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
⊢ ε • ↑↑ν (A ∩ E) = ↑ε * ↑↑ν (A ∩ E)
rfl
case ha
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ¬↑↑(ε • ν) (A ∩ E) = ⊤ ∧ ¬↑↑(withDensity ν ξ) (A ∩ E) = ⊤
case ha
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E) ≠ ⊤
rw [Ne.def, ENNReal.add_eq_top, not_or]
no goals
case ha
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ¬↑↑(ε • ν) (A ∩ E) = ⊤ ∧ ¬↑↑(withDensity ν ξ) (A ∩ E) = ⊤
exact ⟨ne_of_lt (measure_lt_top _ _), ne_of_lt (measure_lt_top _ _)⟩
no goals
case hb
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E) + ↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑μ (A ∩ E) ≠ ⊤
exact ne_of_lt (measure_lt_top _ _)
no goals
case ha
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E)) + ENNReal.toReal (↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑(ε • ν) (A ∩ E) ≠ ⊤
exact ne_of_lt (measure_lt_top _ _)
no goals
case hb
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : ENNReal.toReal (↑↑(ε • ν) (A ∩ E)) + ENNReal.toReal (↑↑(withDensity ν ξ) (A ∩ E)) ≤ ENNReal.toReal (↑↑μ (A ∩ E))
⊢ ↑↑(withDensity ν ξ) (A ∩ E) ≠ ⊤
exact ne_of_lt (measure_lt_top _ _)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : 0 ≤ ENNReal.toReal (↑↑μ (A ∩ E) - ↑↑(withDensity ν ξ) (A ∩ E)) - ENNReal.toReal (↑↑(ε • ν) (A ∩ E))
⊢ (∫⁻ (a : α) in A ∩ E, ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : 0 ≤ ENNReal.toReal (↑↑μ (A ∩ E) - ↑↑(withDensity ν ξ) (A ∩ E)) - ENNReal.toReal (↑↑(ε • ν) (A ∩ E))
⊢ ↑↑(withDensity ν ξ) (A ∩ E) ≤ ↑↑μ (A ∩ E)
rw [withDensity_apply _ (hA.inter hE₁)]
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
A : Set α
hA : MeasurableSet A
this : 0 ≤ ENNReal.toReal (↑↑μ (A ∩ E) - ↑↑(withDensity ν ξ) (A ∩ E)) - ENNReal.toReal (↑↑(ε • ν) (A ∩ E))
⊢ (∫⁻ (a : α) in A ∩ E, ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
exact hξle (A ∩ E) (hA.inter hE₁)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (ξ + indicator E fun x => ↑ε) x ∂ν) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
⊢ (ξ + indicator E fun x => ↑ε) ∈ measurableLE ν μ
refine' ⟨Measurable.add hξm (Measurable.indicator measurable_const hE₁), fun A hA => _⟩
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  (∫⁻ (a : α) in A, (ξ + indicator E fun x => ↑ε) a ∂ν) =
    (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ (∫⁻ (x : α) in A, (ξ + indicator E fun x => ↑ε) x ∂ν) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (ξ + indicator E fun x => ↑ε) x ∂ν) ≤ ↑↑μ A
have :
  (∫⁻ a in A, (ξ + E.indicator fun _ => (ε : ℝ≥0∞)) a ∂ν) =
    (∫⁻ a in A ∩ E, ε + ξ a ∂ν) + ∫⁻ a in A \ E, ξ a ∂ν := by
  simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
    set_lintegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, Pi.add_apply,
    lintegral_indicator _ hE₁, restrict_apply hE₁]
  rw [inter_comm, add_comm]
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  (∫⁻ (a : α) in A, (ξ + indicator E fun x => ↑ε) a ∂ν) =
    (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ ((∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν) ≤ ↑↑μ (A ∩ E) + ↑↑μ (A \ E)
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  (∫⁻ (a : α) in A, (ξ + indicator E fun x => ↑ε) a ∂ν) =
    (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ (∫⁻ (x : α) in A, (ξ + indicator E fun x => ↑ε) x ∂ν) ≤ ↑↑μ A
rw [this, ← measure_inter_add_diff A hE₁]
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this✝ : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  (∫⁻ (a : α) in A, (ξ + indicator E fun x => ↑ε) a ∂ν) =
    (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ ((∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν) ≤ ↑↑μ (A ∩ E) + ↑↑μ (A \ E)
exact add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁))
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν) + ↑ε * ↑↑ν (E ∩ A) =
    ↑ε * ↑↑ν (A ∩ E) + ∫⁻ (a : α) in A, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, (ξ + indicator E fun x => ↑ε) a ∂ν) =
    (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) + ∫⁻ (a : α) in A \ E, ξ a ∂ν
simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
  set_lintegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, Pi.add_apply,
  lintegral_indicator _ hE₁, restrict_apply hE₁]
no goals
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
h : ¬(μ₁, ξ).fst ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ↑↑ν E
hE₃ :
  VectorMeasure.restrict 0 E ≤
    VectorMeasure.restrict (toSignedMeasure (μ - withDensity ν ξ) - toSignedMeasure (ε • ν)) E
hξle : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A, ξ a ∂ν) ≤ ↑↑μ A
hε₂ : ∀ (A : Set α), MeasurableSet A → (∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν) ≤ ↑↑μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν) + ↑ε * ↑↑ν (E ∩ A) =
    ↑ε * ↑↑ν (A ∩ E) + ∫⁻ (a : α) in A, iSup (fun n => ⨆ (k : ℕ) (_ : k ≤ n), f k) a ∂ν
rw [inter_comm, add_comm]
case refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ μ = (μ - withDensity ν ξ, ξ).fst + withDensity ν (μ - withDensity ν ξ, ξ).snd
case refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ μ = (μ₁, ξ).fst + withDensity ν (μ₁, ξ).snd
rw [hμ₁]
case refine'_2.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑μ A = ↑↑((μ - withDensity ν ξ, ξ).fst + withDensity ν (μ - withDensity ν ξ, ξ).snd) A
case refine'_2
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
⊢ μ = (μ - withDensity ν ξ, ξ).fst + withDensity ν (μ - withDensity ν ξ, ξ).snd
ext1 A hA
no goals
case refine'_2.h
α : Type u_1
β : Type ?u.139824
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ) (k : ℕ) (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
μ₁ : Measure α := μ - withDensity ν ξ
hμ₁ : μ₁ = μ - withDensity ν ξ
hle : withDensity ν ξ ≤ μ
this : IsFiniteMeasure (withDensity ν ξ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑μ A = ↑↑((μ - withDensity ν ξ, ξ).fst + withDensity ν (μ - withDensity ν ξ, ξ).snd) A
rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
  add_tsub_cancel_of_le (hle A hA)]