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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : α → E
μ : Measure α
⊢ lpNorm (n • f) p μ = n • lpNorm f p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : α → E
μ : Measure α
⊢ lpNorm (n • f) p μ = ↑n * lpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace ℝ 𝕜
n : ℕ
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (↑n * f) p μ = ↑n * lpNorm f p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace ℝ 𝕜
n : ℕ
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (↑n * f) p μ = ↑n * lpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace ℝ 𝕜
f : α → 𝕜
n : ℕ
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (f * ↑n) p μ = lpNorm f p μ * ↑n

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace ℝ 𝕜
f : α → 𝕜
n : ℕ
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (f * ↑n) p μ = lpNorm f p μ * ↑n
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
⊢ lpNorm (f - g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
⊢ lpNorm (f + -g) p μ ≤ lpNorm f p μ + lpNorm g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (f - g) p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (f - g) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (g - f) p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (g - f) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm (f + g) p μ + lpNorm g p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm (f + g) p μ + lpNorm g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g h : α → E
hf : MemLp f p μ
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm (f - h) p μ ≤ lpNorm (f - g) p μ + lpNorm (g - h) p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g h : α → E
hf : MemLp f p μ
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm (f - h) p μ ≤ lpNorm (f - g) p μ + lpNorm (g - h) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case hb
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ ∑ i ∈ s, eLpNorm (f i) p μ ≠ ∞

Tactic:
simpa using

Goal state after:
case hb
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ ∀ x ∈ s, ¬eLpNorm (f x) p μ = ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.posPart = s.toJordanDecomposition.posPart.singularPart μ

pp: case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ

Tactic:
· have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by fun_prop
    refine eq_singularPart hfpos htμ.1 ?_
    rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

Goal state after:
case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case pos.hf
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable ((starRingEnd (α → K)) f) μ

Tactic:
exact (continuous_star.measurable.comp_aemeasurable hf.aemeasurable).aestronglyMeasurable

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

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

Tactic:
simpa using

Goal state after:
case refine_1
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i ↦ (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, (fs n) a ≤ c
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

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

Tactic:
simpa using

Goal state after:
case refine_2
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i ↦ (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun a_1 ↦ (fs a_1) a) L (𝓝 (f a))
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
δ : ℝ
δ_pos : 0 < δ
x : Ω
⊢ ‖↑((thickenedIndicator δ_pos F) x)‖ ≤ 1

Tactic:
simpa using

Goal state after:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
δ : ℝ
δ_pos : 0 < δ
x : Ω
⊢ (thickenedIndicatorAux δ F x).toNNReal ≤ 1
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h : Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F))
n : ℕ
⊢ ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ = ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)

Tactic:
lintegral_coe_eq_integral

Goal state after:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h : Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F))
n : ℕ
⊢ ENNReal.ofReal (∫ (a : Ω), ↑((thickenedIndicator ⋯ F) a) ∂μ) = ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)

case hfi
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h : Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F))
n : ℕ
⊢ Integrable (fun x ↦ ↑((thickenedIndicator ⋯ F) x)) μ
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 μ
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Tactic:
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.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hm : ¬m ≤ m0
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : ¬m ≤ m0
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α) in s, |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ 0 ≤ ∫ (x : α) in s, |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : Integrable f μ
hsig : ¬SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : Integrable f μ
hsig : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ ∫ (x : α) in s, |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : ¬m ≤ m0
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : Integrable f μ
hsig : ¬SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : Integrable f μ
hsig : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : (fun μ s ↦ (↑μ s).toNNReal) μ = (fun μ s ↦ (↑μ s).toNNReal) ν
s : Set Ω
x✝ : MeasurableSet s
⊢ ↑μ s = ↑ν s

Tactic:
simpa using

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : (fun μ s ↦ (↑μ s).toNNReal) μ = (fun μ s ↦ (↑μ s).toNNReal) ν
s : Set Ω
x✝ : MeasurableSet s
⊢ ↑μ s = ↑ν s
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
μ : ProbabilityMeasure Ω
f : ι → Set Ω
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
μ : ProbabilityMeasure Ω
f : ι → Set Ω
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

Tactic:
simpa using

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
⊢ μ s ≤ 1
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
s✝ t : Set Ω
μ ν : FiniteMeasure Ω
h : (fun μ s ↦ (↑μ s).toNNReal) μ = (fun μ s ↦ (↑μ s).toNNReal) ν
s : Set Ω
x✝ : MeasurableSet s
⊢ ↑μ s = ↑ν s

Tactic:
simpa using

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s✝ t : Set Ω
μ ν : FiniteMeasure Ω
h : (fun μ s ↦ (↑μ s).toNNReal) μ = (fun μ s ↦ (↑μ s).toNNReal) ν
s : Set Ω
x✝ : MeasurableSet s
⊢ ↑μ s = ↑ν s
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

Tactic:
simpa using

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

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

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hfint : ¬Integrable f μ
⊢ 0 ≤ ∫ (x : α), ‖f x‖ ∂μ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
μ : FiniteMeasure Ω
f : ι → Set Ω
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
μ : FiniteMeasure Ω
f : ι → Set Ω
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))
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
hfint : Integrable f μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ

Tactic:
simpa using

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