mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
⊢ Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)

Tactic:
refine tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ {x | ↑n ≤ ↑‖f x‖₊}.indicator f x = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ v (A ∪ B \ A) = v B

Tactic:
Set.union_sdiff_cancel h

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ v B = v B
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
J : v (⋂ n, s n) = v univ - v (⋃ n, (s n)ᶜ)
i j : ℕ
hij : i ≤ j
⊢ (s i)ᶜ ⊆ (s j)ᶜ

Tactic:
by simpa using hm hij

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (ofMeasurable (fun s x ↦ v s) ⋯ ⋯) s = v s

Tactic:
ofMeasurable_apply _ hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ v s = v s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  (μ.restrict (sets n))[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (μ.restrict (sets n))[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun x ↦ (B (f x)) (μ[g | m] x)

Tactic:
filter_upwards [this, (condExp_restrict_ae_eq_restrict hm (h_meas n) hg)] with ω hω1 hω2

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  (μ.restrict (sets n))[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)
ω : Ω
hω1 : (μ.restrict (sets n))[fun ω ↦ (B (f ω)) (g ω) | m] ω = (B (f ω)) ((μ.restrict (sets n))[g | m] ω)
hω2 : (μ.restrict (sets n))[g | m] ω = μ[g | m] ω
⊢ (μ.restrict (sets n))[fun ω ↦ (B (f ω)) (g ω) | m] ω = (B (f ω)) (μ[g | m] ω)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case pos
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ (μ.restrict (sets n))[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)

Tactic:
suffices (μ.restrict (sets n))[fun ω ↦ B ((sets n).indicator f ω) (g ω) | m]
      =ᵐ[μ.restrict (sets n)] fun ω ↦ B ((sets n).indicator f ω) ((μ.restrict (sets n))[g | m] ω) by
    refine EventuallyEq.trans (condExp_congr_ae ?_) (this.trans ?_)
    · filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω hω
      rw [hω]
    · filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω hω
      rw [hω]

Goal state after:
case pos
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ (μ.restrict (sets n))[fun ω ↦ (B ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • j).toSignedMeasure i = (r • j.toSignedMeasure) i

Tactic:
rw [_root_.smul_apply, toSignedMeasure, toSignedMeasure,
    toSignedMeasure_sub_apply hi, toSignedMeasure_sub_apply hi, smul_sub, smul_posPart,
    smul_negPart, measureReal_nnreal_smul_apply, measureReal_nnreal_smul_apply]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑r * j.posPart.real i - ↑r * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real i
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδpos, hδ⟩ := hf.eLpNorm_indicator_le' hp_one hp_top hmeas (half_pos hε)
  refine ⟨δ, hδpos, fun s hs hμs => le_trans (hδ s hs hμs) ?_⟩
  rw [ENNReal.ofReal_div_of_pos zero_lt_two, (by simp : ENNReal.ofReal 2 = 2),
      ENNReal.mul_div_cancel] <;>
    norm_num

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
· exact Or.inl ⟨hxu', hx⟩

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case e'_5
α : Type u_1
m✝ : MeasurableSpace α
μ✝ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
n : ℕ
⊢ (if MeasurableSet (s n) then ∫ (x : α) in s n, f x ∂μ else 0) = ∫ (x : α) in s n, f x ∂μ

pp: case e'_6
α : Type u_1
m✝ : MeasurableSpace α
μ✝ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
⊢ (if MeasurableSet (⋃ i, s i) then ∫ (x : α) in ⋃ i, s i, f x ∂μ else 0) = ∫ (x : α) in ⋃ n, s n, f x ∂μ

Tactic:
· rw [if_pos (hs₁ n)]

Goal state after:
case e'_6
α : Type u_1
m✝ : MeasurableSpace α
μ✝ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
⊢ (if MeasurableSet (⋃ i, s i) then ∫ (x : α) in ⋃ i, s i, f x ∂μ else 0) = ∫ (x : α) in ⋃ n, s n, f x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (-s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]
    infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case refine_1.left
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (fun x ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ

Tactic:
apply Measurable.aestronglyMeasurable

Goal state after:
case refine_1.left
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ ENNReal.ofReal (ε.toReal / 3 * (1 / ↑(measureUnivNNReal μ) ^ (1 / p.toReal) * (μ tᶜ).toReal ^ (1 / p.toReal))) ≤
    ENNReal.ofReal (ε.toReal / 3)

Tactic:
refine ENNReal.ofReal_le_ofReal (mul_le_of_le_one_right hε'.le ?_)
      rw [mul_comm, mul_one_div, div_le_one]
      · gcongr
        refine (ENNReal.toReal_le_of_le_ofReal (measureUnivNNReal_pos hμ).le ?_)
        rw [ENNReal.ofReal_coe_nnreal, coe_measureUnivNNReal]
        exact measure_mono (Set.subset_univ _)
      · exact Real.rpow_pos_of_pos (measureUnivNNReal_pos hμ) _

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case refine_2.left
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (fun x ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
apply Measurable.aestronglyMeasurable

Goal state after:
case refine_2.left
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ (μ.withDensityᵥ f) j = 0

Tactic:
withDensityᵥ_apply hfi (hm _ hj₁)

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s ≪ᵥ μ.toENNRealVectorMeasure
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
    totalVariation_absolutelyContinuous_iff] at h

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
· congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i).re + ((μ.withDensityᵥ (c.rnDeriv μ)) i).re = { re := (re c) i, im := (im c) i }.re

Tactic:
withDensityᵥ_apply (c.integrable_rnDeriv μ) hi,

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i).re + (∫ (x : α) in i, c.rnDeriv μ x ∂μ).re = { re := (re c) i, im := (im c) i }.re
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i).im + ((μ.withDensityᵥ (c.rnDeriv μ)) i).im = { re := (re c) i, im := (im c) i }.im

Tactic:
withDensityᵥ_apply (c.integrable_rnDeriv μ) hi,

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i).im + (∫ (x : α) in i, c.rnDeriv μ x ∂μ).im = { re := (re c) i, im := (im c) i }.im
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : BorelSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
key : ∀ {F : Set Ω}, IsClosed[inst✝³] F → μ F = ν F
⊢ μ = ν

Tactic:
apply ext_of_generate_finite _ ?_ isPiSystem_isClosed

Goal state after:
case hμν
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : BorelSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
key : ∀ {F : Set Ω}, IsClosed[inst✝³] F → μ F = ν F
⊢ ∀ s ∈ {s | IsClosed[inst✝³] s}, μ s = ν s

case h_univ
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : BorelSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
key : ∀ {F : Set Ω}, IsClosed[inst✝³] F → μ F = ν F
⊢ μ univ = ν univ

Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : BorelSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
key : ∀ {F : Set Ω}, IsClosed[inst✝³] F → μ F = ν F
⊢ inst✝⁴ = MeasurableSpace.generateFrom {s | IsClosed[inst✝³] s}
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
⊢ μ s ≤ 1

Tactic:
simpa using apply_mono μ (subset_univ s)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto (fun i ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass :=
    isOpen_compl_singleton.mem_nhds (μ.mass_nonzero_iff.mpr nonzero)

Goal state after:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
⊢ Tendsto (fun i ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UniformIntegrable f p μ

Tactic:
refine ⟨fun i => (hf i).aestronglyMeasurable,
    unifIntegrable_of hp hp' (fun i => (hf i).aestronglyMeasurable) h, ?_⟩
  obtain ⟨C, hC⟩ := h 1 one_pos
  refine ⟨((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1).toNNReal, fun i => ?_⟩
  calc
    eLpNorm (f i) p μ ≤
        eLpNorm ({ x : α | ‖f i x‖₊ < C }.indicator (f i)) p μ +
          eLpNorm ({ x : α | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ := by
      refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx
    _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by
      have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
      refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
      simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
      exact le_rfl
    _ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by
      rw [ENNReal.coe_toNNReal (by finiteness)]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case refine_1.refine_2
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ 𝕜
⊢ Tendsto (fun i ↦ ↑(∫ (x : Ω), RCLike.im (f x) ∂↑(μs i)) * RCLike.I) F
    (𝓝 (↑(∫ (x : Ω), RCLike.im (f x) ∂↑μ) * RCLike.I))

Tactic:
exact (Tendsto.comp (RCLike.continuous_ofReal.tendsto _)
        (h (f.comp RCLike.im RCLike.lipschitzWith_im))).mul_const _

Goal state after: