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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
⊢ 0 ≤ s (⋃ (_ : l < k), s.restrictNonposSeq i l)

Tactic:
· convert! le_of_eq s.empty.symm
      ext; simp only [exists_prop, Set.mem_empty_iff_false, Set.mem_iUnion, not_and, iff_false]
      exact fun h' => False.elim (h h')

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0
⊢ v ≪ᵥ w

Tactic:
intro s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0
s : Set α
hs : w s = 0
⊢ v s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ -v ≪ᵥ w

Tactic:
intro s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (-v) s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ v ≪ᵥ -w

Tactic:
intro s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (-w) s = 0
⊢ v s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ + v₂ ≪ᵥ w

Tactic:
intro s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (v₁ + v₂) s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ - v₂ ≪ᵥ w

Tactic:
intro s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (v₁ - v₂) s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ r • v ≪ᵥ w

Tactic:
intro s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (r • v) s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
⊢ ∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0

Tactic:
intro s hs

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : μ.ennrealToMeasure s = 0
⊢ v s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ) = j₂.posPart.real (i ∩ Tᶜ)

Tactic:
rw [measureReal_union, measureReal_def,
      show j₂.posPart (i ∩ T) = 0 from
        nonpos_iff_eq_zero.1 (hT₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]

Goal state after:
case hd
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ Disjoint (i ∩ T) (i ∩ Tᶜ)

case h
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ MeasurableSet (i ∩ Tᶜ)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case neg.posPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (-(-r • s)).toJordanDecomposition.posPart = (-r).toNNReal • s.toJordanDecomposition.negPart

Tactic:
toJordanDecomposition_neg,

Goal state after:
case neg.posPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (-(-r • s).toJordanDecomposition).posPart = (-r).toNNReal • s.toJordanDecomposition.negPart
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case neg.negPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (-(-r • s)).toJordanDecomposition.negPart = (-r).toNNReal • s.toJordanDecomposition.posPart

Tactic:
toJordanDecomposition_neg,

Goal state after:
case neg.negPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (-(-r • s).toJordanDecomposition).negPart = (-r).toNNReal • s.toJordanDecomposition.posPart
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
⊢ v.trim ⋯ = v

Tactic:
by
  ext i hi
  exact if_pos hi

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
⊢ trim 0 hle = 0

Tactic:
by
  ext i hi
  exact if_pos hi

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
hfg : Integrable (fun x ↦ (f x).toReal • g x) μ
⊢ (μ.withDensityᵥ fun x ↦ (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g

Tactic:
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    ← withDensityᵥ_smul_eq_withDensityᵥ_withDensity hf.ennreal_toNNReal hfg]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
hfg : Integrable (fun x ↦ (f x).toReal • g x) μ
⊢ (μ.withDensityᵥ fun x ↦ (f x).toReal • g x) = μ.withDensityᵥ ((fun x ↦ (f x).toNNReal) • g)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : μ.withDensityᵥ f = μ.withDensityᵥ g
i : Set α
hi : MeasurableSet i
x✝ : μ i < ∞
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ

Tactic:
← withDensityᵥ_apply hf hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : μ.withDensityᵥ f = μ.withDensityᵥ g
i : Set α
hi : MeasurableSet i
x✝ : μ i < ∞
⊢ (μ.withDensityᵥ f) i = ∫ (x : α) in i, g x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ (μ.withDensityᵥ f) i = (μ.withDensityᵥ g) i

Tactic:
rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

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

Tactic:
toJordanDecomposition_neg,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (-s.toJordanDecomposition).posPart.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

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

Tactic:
toJordanDecomposition_neg,

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

Tactic:
rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0
hp : p ≠ 0
hf : AEStronglyMeasurable f μ
⊢ lpNorm f (↑p) μ = (∫ (x : α), ‖f x‖ ^ ↑p ∂μ) ^ (↑p)⁻¹

Tactic:
by
  rw [lpNorm_eq_integral_norm_rpow_toReal (by positivity) (by simp) hf]; simp

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

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

pp: case neg
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm ((starRingEnd (α → K)) f) p μ = lpNorm f p μ

Tactic:
· rw [← lpNorm_norm hf, ← lpNorm_norm]
    · simp
    · exact (continuous_star.measurable.comp_aemeasurable hf.aemeasurable).aestronglyMeasurable

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

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
⊢ ∀ (n : ℕ), ∀ x ∈ F, 1 ≤ ((fun n ↦ thickenedIndicator ⋯ F) n) x

pp: case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
⊢ Tendsto (fun n x ↦ ((fun n ↦ thickenedIndicator ⋯ F) n) x) atTop (𝓝 (F.indicator fun x ↦ 1))

Tactic:
· exact fun n x hxF ↦ one_le_thickenedIndicator_apply X Nat.one_div_pos_of_nat hxF

Goal state after:
case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
⊢ Tendsto (fun n x ↦ ((fun n ↦ thickenedIndicator ⋯ F) n) x) atTop (𝓝 (F.indicator fun x ↦ 1))
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  ∀ (x : X),
    Tendsto (fun i ↦ (thickenedIndicator ⋯ F) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun x ↦ 1) x))
x : X
⊢ Tendsto (fun i ↦ ((fun n ↦ thickenedIndicator ⋯ F) i) x) atTop (𝓝 ((closure[inst✝¹] F).indicator (fun x ↦ 1) x))

Tactic:
exact key x

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

Goal state before:

Tactic:
_ ≤ ∫ x in s, μ[(fun x => ‖f x‖ ^ p) | m] x ∂μ := by
    refine integral_mono_of_nonneg ?_ ?_ ?_
    · filter_upwards with a using by positivity
    · exact integrable_condExp.congr (condExp_restrict_ae_eq_restrict hm hs hf)
    · exact ae_restrict_le (Integrable.norm_condExp_rpow_le hp hf)
  _ ≤ _ := by
    apply setIntegral_condExp_le_of_ae_nonneg hs
    filter_upwards with ω using by positivity

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:
simpa only [← ENNReal.coe_add] using (by exact_mod_cast le')

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
  intro ε hε
  obtain ⟨δ, hδ, hδ'⟩ := hUI hε
  refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩
  refine Lp.eLpNorm_le_of_ae_tendsto
    (Eventually.of_forall (f := u) fun n => hδ' (s n) t ht ht') ?_ ?_
  · exact fun n => (hfn (s n)).indicator ht
  · filter_upwards [hs] with a ha
    by_cases memt : a ∈ t
    · simpa [memt]
    · simp [memt]

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

Goal state before:
pp: case neg
Ω : 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
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
fun i ↦ (μs i).testAgainstNN_eq_mass_mul f,

Goal state after:
case neg
Ω : 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
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun i ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

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

Tactic:
exact continuous_testAgainstNN_eval 1

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 μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p = ∞
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
by_cases! h : MemLp μ[f | m] ⊤ μ
        · simp_all only [lpNorm_exponent_top_eq_essSup]
          exact hf.essSup_norm_condExp_le_essSup_norm
        · simp_all

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ (↑((μs i).testAgainstNN f)).toNNReal) F (𝓝 (↑(μ.testAgainstNN f)).toNNReal)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun a ↦ (μs a).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
ENNReal.toNNReal_coe

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | ↑C ≤ ↑‖μ[g | ℱ n] x‖₊} * ↑C ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1
⊢ μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ

Tactic:
←
      ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | ↑C ≤ ↑‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ