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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hsv : s ≤[v] 0
hs : s (u ∆ v) = 0
⊢ s (w ∩ u) = s (w ∩ v)

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
  rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv
  have := of_inter_eq_of_symmDiff_eq_zero_positive hu hv hw hsu hsv
  simp only [neg_apply, neg_inj, neg_eq_zero] at this
  exact this hs

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 : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ v ≪ᵥ -w

Tactic:
by
  intro s hs
  rw [neg_apply, neg_eq_zero] at hs
  exact h hs

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 : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [withDensityᵥ, dif_pos hf]; exact dif_pos hs

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 : α → E
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Tactic:
by
  by_cases hf : Integrable f μ
  · ext1 i hi
    rw [_root_.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
      withDensityᵥ_apply hf.neg hi]
    simp only [Pi.neg_apply]
  · rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]
    rwa [integrable_neg_iff]

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 g : α → E
hf : Integrable f μ
hg : Integrable g μ
⊢ μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]

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 fun x ↦ ↑(f x).toNNReal).withDensityᵥ g

Tactic:
← 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.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ s).toReal ≤ (ν s).toReal ↔ μ s ≤ ν s

Tactic:
apply ENNReal.toReal_le_toReal

Goal state after:
case ha
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ μ s ≠ ∞

case hb
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ ν s ≠ ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

pp: case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
· congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

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

Tactic:
withDensityᵥ_neg,

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ

Tactic:
by
  convert_to ∫⁻ x, (F.indicator (fun _ ↦ (1 : ℝ≥0∞))) x ∂μ ≤ ∫⁻ x, hF.apprSeq n x ∂μ
  · rw [lintegral_indicator hF.measurableSet]
    simp only [lintegral_one, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
  · apply lintegral_mono
    intro x
    by_cases hxF : x ∈ F
    · simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n hxF, ENNReal.coe_one, le_refl]
    · simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]

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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ μ.real {x | ↑R < |μ[f | m] x|} * ↑R < μ.real {x | ↑R < |μ[f | m] x|} * ↑R

Tactic:
refine lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_

Goal state after:
case pos.refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ IntegrableOn (fun x ↦ |μ[f | m] x|) {x | ↑R < |μ[f | m] x|} μ

case pos.refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ ∫ (x : α) in {x | ↑R < |μ[f | m] x|}, |μ[f | m] x| ∂μ ≤ μ.real {x | ↑R < |μ[f | m] x|} * ↑R
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i ↦ (μs i) E) L ≤ μ E
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E
⊢ μ Eᶜ ≤ liminf (fun i ↦ (μs i) Eᶜ) L

Tactic:
meas_Ec,

Goal state after:
case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i ↦ (μs i) E) L ≤ μ E
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E
⊢ 1 - μ E ≤ liminf (fun i ↦ (μs i) Eᶜ) L
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) L
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ

Tactic:
meas_Ec,

Goal state after:
case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) L
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ 1 - μ E
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : IsTightMeasureSet (Measure.fst '' μ)
hμ₂ : IsTightMeasureSet (Measure.snd '' μ)
⊢ IsTightMeasureSet μ

Tactic:
rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le] at hμ₁ hμ₂ ⊢
  intro ε hε
  obtain ⟨K₁, hK₁_compact, hK₁_le⟩ := hμ₁ (ε / 2) (by aesop)
  obtain ⟨K₂, hK₂_compact, hK₂_le⟩ := hμ₂ (ε / 2) (by aesop)
  refine ⟨K₁ ×ˢ K₂, hK₁_compact.prod hK₂_compact, fun κ hκ_mem ↦ ?_⟩
  grw [compl_prod_eq_union, measure_union_le, ← ENNReal.add_halves (a := ε)]
  apply add_le_add
  · specialize hK₁_le _ <| mem_image_of_mem _ hκ_mem
    grw [Measure.fst, ← Measure.le_map_apply (by fun_prop)] at hK₁_le
    simpa [prod_univ] using hK₁_le
  · specialize hK₂_le _ <| Set.mem_image_of_mem _ hκ_mem
    grw [Measure.snd, ← Measure.le_map_apply (by fun_prop)] at hK₂_le
    simpa [univ_prod] using hK₂_le

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

Goal state before:
pp: case refine_3
α : 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 μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
⊢ ∃ C, ∀ (i : ℕ), eLpNorm ((fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) i) p μ ≤ ↑C

Tactic:
obtain ⟨C, hC⟩ := hf₃

Goal state after:
case refine_3
α : 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
⊢ ∃ C, ∀ (i : ℕ), eLpNorm ((fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) i) p μ ≤ ↑C
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
hi2 : i ∉ p2
⊢ g i ∈ s i

Tactic:
g,

Goal state after:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
hi2 : i ∉ p2
⊢ ((if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) ∈ s i
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi2 : i ∈ p2
hi1 : i ∉ p1
⊢ g i ∈ s i

Tactic:
g,

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi2 : i ∈ p2
hi1 : i ∉ p1
⊢ ((if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) ∈ s i
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2.refine_3
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : μ u < ⊤
⊢ ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ

Tactic:
specialize h hu hs ht

Goal state after:
case refine_2.refine_3
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (u ×ˢ s ×ˢ t) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (u ×ˢ s ×ˢ t)
hu : MeasurableSet u
hμu : μ u < ⊤
⊢ ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g κ μ ↔ (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)

Tactic:
classical
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [Measure.ext_prod₃_iff]
    intro u s t hu hs ht
    rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
      Measure.compProd_apply (hu.prod (hs.prod ht))]
    refine lintegral_congr_ae ?_
    have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
    simp_rw [h_set_eq]
    filter_upwards [h s t hs ht] with ω hω
    by_cases hωu : ω ∈ u
    swap; · simp [hωu]
    simp only [hωu, ↓reduceIte]
    rw [map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht),
      mk_preimage_prod, hω, prod_apply_prod, map_apply' _ (by fun_prop), map_apply' _ (by fun_prop)]
    exacts [ht, hs]
  · intro s t hs ht
    rw [Measure.ext_prod₃_iff] at h
    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_
    · exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))
    · exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))
    intro u hu hμu
    specialize h hu hs ht
    rw [Measure.compProd_apply_prod hu (hs.prod ht),
      Measure.compProd_apply_prod hu (hs.prod ht)] at h
    convert! h with ω ω
    · rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
    · rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]

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

Goal state before:
pp: case e'_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ generateFrom {s i} = generateFrom {t | ∃ n ∈ {i}, s n = t}

Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left, Set.ofPred_eq_eq_singleton']

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

Goal state before:
pp: case e'_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ generateFrom {s k} = generateFrom {t | ∃ n ∈ {k}, s n = t}

Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left, Set.ofPred_eq_eq_singleton']

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
i : ι
hi : i ∈ S
⊢ sets_t' i = univ

Tactic:
sets_t',

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
i : ι
hi : i ∈ S
⊢ (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ) = univ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
lintegral_indicator (hMf _ h_meas_s'),

Goal state after:
case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ ENNReal.ofReal Var[X; μ] = eVar[X; μ]

Tactic:
rw [variance, ENNReal.ofReal_toReal]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * Y a) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

Tactic:
· exact integrable_const _

Goal state after:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * Y a) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c‖ₑ ^ 2 * ‖X ω - ∫ (a : Ω), X a ∂μ‖ₑ ^ 2 = ENNReal.ofReal (c ^ 2) * ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2

Tactic:
← enorm_pow,

Goal state after:
case e_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c ^ 2‖ₑ * ‖X ω - ∫ (a : Ω), X a ∂μ‖ₑ ^ 2 = ENNReal.ofReal (c ^ 2) * ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2