mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ MeasurableSet {μ | IsProbabilityMeasure μ}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
⊢ ⇑(μ + ν) = ⇑μ + ⇑ν

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ p ≠ 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
⊢ ⇑(c • μ) = c • ⇑μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
s : Set Ω
⊢ (c • μ) s = c • μ s

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ (μ.restrict A) s = μ (s ∩ A)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ (μ.restrict A).mass = μ A

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.restrict univ = μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : ¬m ≤ m0
x : α
⊢ 0 x ≤ ‖f x‖ ^ p

Tactic:
by

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

Goal state before:
pp: case hg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ↑a.2 v

Tactic:
exact (Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd)

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s t : Set Ω
h : Disjoint s t
ht : MeasurableSet t
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable fun μ ↦ (↑μ.1).prod ↑μ.2

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
f : ℕ → Set Ω
hf : Summable fun n ↦ μ (f n)
⊢ μ (⋃ n, f n) ≤ ∑' (n : ℕ), μ (f n)

Tactic:
by

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 : ι), 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 : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
x : α
⊢ 0 x ≤ ‖f x‖ ^ p

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ 𝕜), Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
X : Type u_2
inst✝ : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
⊢ Continuous[inst✝, instTopologicalSpace] μs ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Continuous[inst✝, _] fun x ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)

Tactic:
by

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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UnifIntegrable f p μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ i ∈ T, s i) = ∑ i ∈ T, μ.restrict (s i)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A = 0 ↔ μ A = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
X : Type u_2
inst✝ : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
⊢ Continuous[inst✝, instTopologicalSpace] μs ↔ ∀ (f : Ω →ᵇ ℝ), Continuous[inst✝, _] fun x ↦ ∫ (ω : Ω), f ω ∂↑(μs x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A ≠ 0 ↔ μ A ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
a : α
⊢ 0 a ≤ ‖μ[f | m] a‖ ^ p

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
this : {μ | IsFiniteMeasure μ} = (fun μ ↦ μ univ) ⁻¹' Ico 0 ∞
⊢ MeasurableSet {μ | IsFiniteMeasure μ}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ MeasurableSet {μ | IsFiniteMeasure μ}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ¬μ.mass = 0
⊢ IsProbabilityMeasure (μ.mass⁻¹ • ↑μ)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ.mass ≠ 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ μ s = μ.mass * μ.normalize s

Tactic:
by

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∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
⊢ UnifIntegrable (fun f ↦ ↑f) p μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ = μ.mass • μ.normalize.toFiniteMeasure

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
⊢ μ.normalize s = μ.mass⁻¹ * μ s

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable fun μ ↦ (↑μ.1).prod ↑μ.2

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
f : ℕ → Set Ω
hf : Summable fun n ↦ μ (f n)
⊢ μ (⋃ n, f n) ≤ ∑' (n : ℕ), μ (f n)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ↑μ.normalize = μ.mass⁻¹ • ↑μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α) in s, μ[fun x ↦ ‖f x‖ ^ p | m] x ∂μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ μ.toFiniteMeasure.normalize = μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
ω : α
⊢ 0 ω ≤ ‖f ω‖ ^ p

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
c : ℝ≥0
⊢ μ.testAgainstNN (const Ω c) = c * μ.mass

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, μ[fun x ↦ ‖f x‖ ^ p | m] x ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 0 = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 1 = μ.mass

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
⊢ testAgainstNN 0 = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
c : ℝ≥0
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ (c • μ).testAgainstNN f = c • μ.testAgainstNN f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN (c • f) = c • μ.testAgainstNN f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
⊢ μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ f ω ≤ g ω + nndist f g

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
⊢ ↑(f ω) ≤ ↑(g ω + nndist f g)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
⊢ ↑(f ω) ≤ ↑(g ω) + ↑(nndist f g)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
hs : MeasurableSet s
f : α → E
hfint : Integrable f μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ 1) μ

Tactic:
by

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 g : ι → α → β
hf : UniformIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
⊢ UniformIntegrable g p μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
hs : MeasurableSet s
f : α → E
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
this : |↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂)| ≤ ↑μ.mass * dist f₁ f₂
⊢ dist (μ.testAgainstNN f₁) (μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : α → E
hbdd : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ R
hn : {x | ‖f x‖ ≤ R} = ∅
⊢ {x | (fun x ↦ ‖μ[f | m] x‖ ≤ R) x}ᶜ ⊆ Set.univ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
this : ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂
⊢ -(↑μ.mass * dist f₁ f₂) ≤ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : α → E
hbdd : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ R
⊢ ∀ᵐ (x : α) ∂μ, ‖μ[f | m] x‖ ≤ R

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
this : ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂
⊢ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ LipschitzWith μ.mass fun f ↦ μ.testAgainstNN f

Tactic:
by

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 (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous[instTopologicalSpace, _] fun μ ↦ μ.testAgainstNN f

Tactic:
by

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✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
⊢ UniformIntegrable f p μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun μ ↦ μ.mass

Tactic:
by

Goal state after: