mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s A ≤ s (B n)

Tactic:
hA,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s (⋃ n, B n) ≤ s (B n)
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 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal) ≤
    ENNReal.ofReal (ε.toReal / 3)

Tactic:
div_mul_eq_div_mul_one_div,

Goal state after:
α : 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ᶜ ^ (1 / p.toReal) ≤
    ENNReal.ofReal (ε.toReal / 3)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun x ↦ s A) n ≤ s (B n)

Tactic:
hA,

Goal state after:
case a
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun x ↦ s (⋃ n, B n)) n ≤ s (B n)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ (s.toMeasureOfZeroLE i hi₁ hi) univ < ∞

Tactic:
rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ ↑(NNReal.mk (s (i ∩ univ)) ⋯) < ∞
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case h₁
α : 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)
⊢ μ tᶜ ≤ ENNReal.ofReal ↑(measureUnivNNReal μ)

Tactic:
ENNReal.ofReal_coe_nnreal,

Goal state after:
case h₁
α : 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)
⊢ μ tᶜ ≤ ↑(measureUnivNNReal μ)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

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

Tactic:
JordanDecomposition.neg_posPart

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ

Tactic:
exact equivMeasure.right_inv μ

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ singularPart 0 μ = 0

Tactic:
refine (eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left ?_).symm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = 0 + μ.withDensityᵥ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Tactic:
refine
    (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
        ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
        ?_).symm

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ (s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ

Tactic:
refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_
  rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]

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

Goal state before:
pp: case pos
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∈ F
⊢ F.indicator (fun x ↦ 1) x ≤ (fun a ↦ ↑((hF.apprSeq n) a)) x

Tactic:
simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n hxF, ENNReal.coe_one, le_refl]

Goal state after:
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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ ↑C
⊢ ENNReal.ofReal ↑C * μ s ^ p.toReal⁻¹ ≤ ↑C * μ s ^ (1 / p.toReal)

Tactic:
ENNReal.ofReal_coe_nnreal,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ ↑C
⊢ ↑C * μ s ^ p.toReal⁻¹ ≤ ↑C * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
      rwa [Set.mem_ofPred, hx] at hfx

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
hp' : 0 < p
hpt : p = ∞
⊢ MemLp μ[f | m] p μ

Tactic:
simp_all only
    exact memLp_top_of_bound integrable_condExp.1 (essSup (‖f ·‖) μ) hf.ae_norm_condExp_le_essSup

Goal state after:
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 ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖₊ ≤ C
⊢ μ univ ^ p.toReal⁻¹ * ENNReal.ofReal ↑C ≤ ↑C * μ univ ^ p.toReal⁻¹

Tactic:
ENNReal.ofReal_coe_nnreal,

Goal state after:
α : 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 ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖₊ ≤ C
⊢ μ univ ^ p.toReal⁻¹ * ↑C ≤ ↑C * μ univ ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i ↦ (fs i) ω) L (𝓝 (f ω))
⊢ Tendsto (fun i ↦ μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))

Tactic:
apply (ENNReal.tendsto_toNNReal (f.lintegral_lt_top_of_nnreal (μ : Measure Ω)).ne).comp
  exact tendsto_lintegral_nn_filter_of_le_const (Ω := Ω) μ fs_le_const fs_lim

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun ν ↦ ν.map ⋯

Tactic:
continuous_iff_continuousAt

Goal state after:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ ∀ (x : ProbabilityMeasure Ω), ContinuousAt (fun ν ↦ ν.map ⋯) x
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f
⊢ Tendsto (fun n ↦ (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)

Tactic:
have f₀_nn : 0 ≤ ⇑f₀ := fun _ ↦ by
    simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f
f₀_nn : 0 ≤ ⇑f₀
⊢ Tendsto (fun n ↦ (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: case refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
h : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Tactic:
obtain ⟨K, h1, h2⟩ := h ε hε
    exact ⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA μ hμS ↦ (μ.mono hA).trans (h2 μ hμS)⟩

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun ν ↦ ν.map f

Tactic:
continuous_iff_continuousAt

Goal state after:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ ∀ (x : FiniteMeasure Ω), ContinuousAt (fun ν ↦ ν.map f) x
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case hf
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

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

Goal state before:
pp: case hf
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : ↑M
s : Set Ω'
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ Measure.map (fun ω i ↦ X i (ω i)) (Measure.pi μ) = Measure.pi fun i ↦ Measure.map (fun ω ↦ X i (ω i)) (Measure.pi μ)

Tactic:
Measure.pi_map_pi mX

Goal state after:
case refine_2
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ (Measure.pi fun i ↦ Measure.map (X i) (μ i)) = Measure.pi fun i ↦ Measure.map (fun ω ↦ X i (ω i)) (Measure.pi μ)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
⊢ g i ∈ s i

Tactic:
have hi2 : i ∉ p2 := fun hip2 => Set.disjoint_left.mp hST (hp1 hi1) (hp2 hip2)

Goal state after:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
hi2 : i ∉ p2
⊢ g i ∈ s i
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T) η μ

Tactic:
exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = Var[(algebraMap A ℝ) c • X; μ]

pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 • Var[X; μ] = (algebraMap A ℝ) c ^ 2 * Var[X; μ]

Tactic:
· simp only [algebraMap_smul]

Goal state after:
case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 • Var[X; μ] = (algebraMap A ℝ) c ^ 2 * Var[X; μ]