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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
⊢ a ∩ ⋃ i, disjointed f i = a

Tactic:
iUnion_disjointed,

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
⊢ a ∩ ⋃ i, f i = a
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ (s.toMeasureOfLEZero iᶜ ⋯ ⋯) iᶜᶜ = 0

Tactic:
· rw [toMeasureOfLEZero_apply _ _ hi.1.compl hi.1.compl.compl]; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
⊢ v ≤[⋃ b, f b] w

Tactic:
by
  cases nonempty_encodable β
  rw [← Encodable.iUnion_decode₂]
  refine restrict_le_restrict_iUnion v w ?_ ?_
  · intro n
    measurability
  · intro n
    rcases Encodable.decode₂ β n with - | b
    · simp
    · simp [hf₂ b]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
this : Summable fun l ↦ s (s.restrictNonposSeq i l)
n : ℕ
⊢ 0 ≤ 1 / (↑(bdd n) + 1)

pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
this : Summable fun l ↦ s (s.restrictNonposSeq i l)
n : ℕ
⊢ 1 / (↑(bdd n) + 1) ≤ ((fun l ↦ s (s.restrictNonposSeq i l)) ∘ Nat.succ) n

Tactic:
· exact le_of_lt Nat.one_div_pos_of_nat

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
this : Summable fun l ↦ s (s.restrictNonposSeq i l)
n : ℕ
⊢ 1 / (↑(bdd n) + 1) ≤ ((fun l ↦ s (s.restrictNonposSeq i l)) ∘ Nat.succ) n
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:
show r • s = -(-r • s) by rw [neg_smul, neg_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:
show r • s = -(-r • s) by rw [neg_smul, neg_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.Decomposition.Jordan

Goal state before:
pp: case mp.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ s.totalVariation u = 0

pp: case mp.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ t.totalVariation uᶜ = 0

Tactic:
· rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]
      simp [hu₁ _ Set.inter_subset_right]

Goal state after:
case mp.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ t.totalVariation uᶜ = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (s.toJordanDecomposition.posPart i).toReal - s.toJordanDecomposition.negPart.real i =
    (s.toJordanDecomposition.posPart i).toReal - s.toJordanDecomposition.negPart.real i

Tactic:
measureReal_def

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (s.toJordanDecomposition.posPart i).toReal - (s.toJordanDecomposition.negPart i).toReal =
    (s.toJordanDecomposition.posPart i).toReal - (s.toJordanDecomposition.negPart i).toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case pos
α : 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 μ
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
rw [← toReal_eLpNorm (hf.add hg).aestronglyMeasurable,
      ← toReal_eLpNorm hf.aestronglyMeasurable, ← toReal_eLpNorm hg.aestronglyMeasurable,
      ← ENNReal.toReal_add hf.eLpNorm_ne_top hg.eLpNorm_ne_top]

Goal state after:
case pos
α : 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 μ
⊢ (eLpNorm (f + g) p μ).toReal ≤ (eLpNorm f p μ + eLpNorm g p μ).toReal
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case hf
α : 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.1 u

Tactic:
exact (Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ↑μ univ ≠ 0
⊢ (↑μ univ)⁻¹ * ↑μ univ = 1

Tactic:
exact ENNReal.inv_mul_cancel zero μ.prop.measure_univ_lt_top.ne

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

pp: case neg
α : 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 μ
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
· choose _ hf using hf
    set C := (Finset.univ.image fun i : ι => eLpNorm (f i) p μ).max'
      ⟨eLpNorm (f hι.some) p μ, Finset.mem_image.2 ⟨hι.some, Finset.mem_univ _, rfl⟩⟩
    refine ⟨C.toNNReal, fun i => ?_⟩
    rw [ENNReal.coe_toNNReal]
    · exact Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)
    · refine ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)
      rw [Finset.mem_image] at hy
      obtain ⟨i, -, rfl⟩ := hy
      exact hf i

Goal state after:
case neg
α : 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 μ
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ (Measure.comap f ↑μ) univ ≤ ↑μ univ

Tactic:
apply (Measure.comap_apply_le _ _ nullMeasurableSet_univ).trans (measure_mono (subset_univ _))

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_3.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm ((↑n)⁻¹ • f i) p μ ≤ ↑C

Tactic:
simp_rw [eLpNorm_const_smul, ← Finset.mul_sum]

Goal state after:
case refine_3.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ‖(↑n)⁻¹‖ₑ * ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ ↑C
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : TendstoInMeasure μ f u g
⊢ MemLp g p μ

Tactic:
by
  simpa using (hUI.uniformIntegrable_of_tendstoInMeasure u).memLp ⟨g, ⟨fun n => n, htends⟩⟩

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
have hf' : ∀ i ∈ s.image g, f' i ∈ π i := by
    simp_rw [Finset.forall_mem_image, f'_apply]
    exact hf
  filter_upwards [@h (s.image g) f' hf'] with a ha
  simpa [Finset.set_biInter_finset_image, Finset.prod_image hg.injOn, f'_apply] using ha

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

Goal state before:
pp: case pos
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
simp [hi, g]

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

Goal state before:
pp: case neg
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∉ s
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
simp [hi, g]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ f x * (pdf X ℙ volume x).toReal) volume

Tactic:
by
  rw [hasFiniteIntegral_iff_enorm]
  have : (fun x => ‖f x‖ₑ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ := by
    refine ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_
    simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]
    refine .fun_mul (ae_eq_refl _) ?_
    simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
  rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
hp : IsPiSystem p
h_le' : ∀ (i : ι), generateFrom (π i) ≤ _mΩ
hm_p : m_p ≤ _mΩ
⊢ Indep m_p (m a) η μ

Tactic:
exact IndepSets.indep hm_p (h_le a) hp (h_pi a) hS_eq_generate (h_generate a)
        (iIndepSets.piiUnionInter_of_notMem (h_ind.congr η_eq) ha_notin_S)

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬(AEStronglyMeasurable X μ ∧ eLpNorm X 2 μ < ∞)
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ∞

Tactic:
not_and

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ∞
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ∞
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X Y : Ω → ℝ
Z : Ω' ≃ᵐ Ω
⊢ cov[X, Y; Measure.map (⇑Z) μ] = cov[X ∘ ⇑Z, Y ∘ ⇑Z; μ]

Tactic:
by
  simp_rw [covariance, integral_map_equiv, Function.comp_apply]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
this : IsProbabilityMeasure μ
⊢ Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
h.covariance_eq_zero hX hY

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
this : IsProbabilityMeasure μ
⊢ Var[X; μ] + 2 * 0 + Var[Y; μ] = Var[X; μ] + Var[Y; μ]
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, Y; μ] = 0

Tactic:
by_cases h' : ∀ᵐ ω ∂μ, X ω = 0
   · refine integral_eq_zero_of_ae ?_
     filter_upwards [h'] with ω hω
     simp [hω, integral_eq_zero_of_ae h']
   have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
   rw [covariance_eq_sub hX hY, h.integral_mul_eq_mul_integral
       hX.aestronglyMeasurable hY.aestronglyMeasurable, sub_self]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case inr.inl
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hF_lip : LipschitzWith 0 F
⊢ Tendsto (fun n ↦ ∫ (ω : E), F ω ∂Measure.map (Y n) μ'') l (𝓝 (∫ (ω : E), F ω ∂Measure.map Z μ'))

Tactic:
simp only [LipschitzWith.zero_iff] at hF_lip
    specialize hF_lip x₀
    simp only [← hF_lip, integral_const, smul_eq_mul]
    have h_prob n : IsProbabilityMeasure (μ''.map (Y n)) := Measure.isProbabilityMeasure_map (hY n)
    have : IsProbabilityMeasure (μ'.map Z) := Measure.isProbabilityMeasure_map hZ
    simpa using! tendsto_const_nhds

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
a : Ω''
hF_bounded : dist (F (X n a)) (F x₀) ≤ M
⊢ ‖F (X n a)‖ - ‖F x₀‖ ≤ M

Tactic:
exact (abs_sub_abs_le_abs_sub (F (X n a)) (F x₀)).trans hF_bounded

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f g : Filtration ι m
h : ↑f = ↑g
⊢ f = g

Tactic:
cases f; cases g; congr

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
i : ι
hi : i ∈ s
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
simp [hi, g]

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
i : ι
hi : i ∉ s
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
simp [hi, g]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable (limitProcess f ℱ μ)

Tactic:
by
  rw [limitProcess]
  split_ifs with h
  exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]

Goal state after: