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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

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

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ eLpNorm (s.indicator 0) p μ ≤ ENNReal.ofReal ε

pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ f = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ eLpNorm (s.indicator 0) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.restrictNonposSeq i (n✝ + 1) ⊆ i

Tactic:
·

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.restrictNonposSeq i (n✝ + 1) ⊆ 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ f = 0

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ f = 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : p = 0
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : p = 0
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
x✝ : ℕ
⊢ (if MeasurableSet (f x✝) then v (f x✝ ∩ i) else 0) = v (f x✝ ∩ i)

pp: case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (if MeasurableSet (⋃ i, f i) then v ((⋃ i, f i) ∩ i) else 0) = v (⋃ i_1, f i_1 ∩ i)

Tactic:
·

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
x✝ : ℕ
⊢ (if MeasurableSet (f x✝) then v (f x✝ ∩ i) else 0) = v (f x✝ ∩ i)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (if MeasurableSet (⋃ i, f i) then v ((⋃ i, f i) ∩ i) else 0) = v (⋃ i_1, f i_1 ∩ i)

Tactic:
·

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (if MeasurableSet (⋃ i, f i) then v ((⋃ i, f i) ∩ i) else 0) = v (⋃ i_1, f i_1 ∩ i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ μ s ^ p.toReal⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M

pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal M ≠ 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ μ s ^ p.toReal⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v.restrict i) univ = v i

pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v.restrict i) univ = v i

Tactic:
·

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v.restrict i) univ = v i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v.restrict i) univ = v i

Tactic:
·

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v.restrict i) univ = v i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0

pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case refine_1
Ω : 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 ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B (f ω)) (g ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦ (B ((sets n).indicator f ω)) (g ω)

pp: case refine_2
Ω : 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 ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)

Tactic:
·

Goal state after:
case refine_1
Ω : 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 ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B (f ω)) (g ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦ (B ((sets n).indicator f ω)) (g ω)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal M ≠ 0

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal M ≠ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
s : Set α
x : α
m : M
hx : x ∉ s
hs : MeasurableSet s
⊢ (dirac x m).restrict s = 0

pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
s : Set α
x : α
m : M
hx : x ∉ s
hs : ¬MeasurableSet s
⊢ (dirac x m).restrict s = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
s : Set α
x : α
m : M
hx : x ∉ s
hs : MeasurableSet s
⊢ (dirac x m).restrict s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
s : Set α
x : α
m : M
hx : x ∉ s
hs : ¬MeasurableSet s
⊢ (dirac x m).restrict s = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
s : Set α
x : α
m : M
hx : x ∉ s
hs : ¬MeasurableSet s
⊢ (dirac x m).restrict s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.restrictNonposSeq i 0)

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.restrictNonposSeq i 0)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i (n✝ + 1))

Tactic:
·

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i (n✝ + 1))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : MeasurableSet {a}
⊢ v.restrict {a} = dirac a (v {a})

pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : ¬MeasurableSet {a}
⊢ v.restrict {a} = dirac a (v {a})

Tactic:
·

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : MeasurableSet {a}
⊢ v.restrict {a} = dirac a (v {a})
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
h : n < 0
hx₂ : x ∈ s.restrictNonposSeq i 0
⊢ False

pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
h : n < 0
hx₂ : x ∈ s.restrictNonposSeq i 0
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False

Tactic:
·

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : ¬MeasurableSet {a}
⊢ v.restrict {a} = dirac a (v {a})

Tactic:
·

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : ¬MeasurableSet {a}
⊢ v.restrict {a} = dirac a (v {a})
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 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if x ∈ {x | ‖f x‖ < M} then ‖f x‖ else 0) < ?m.95

Tactic:
·

Goal state after:
α : 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 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if x ∈ {x | ‖f x‖ < M} then ‖f x‖ else 0) < ?m.95
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

pp: case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : m < n
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : m < n
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : m < n
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case refine_2
Ω : 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 ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)

Tactic:
·

Goal state after:
case refine_2
Ω : 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 ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (v + w).map f = v.map f + w.map f

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ (v + w).map f = v.map f + w.map f

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (v + w).map f = v.map f + w.map f