mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
⊢ liminf (fun i ↦ (∫⁻ (a : Ω), ENNReal.ofReal (f a) ∂μs i).toReal) atTop =
    (liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop).toReal

Tactic:
have bound : ∀ i, ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i) ≤ nndist 0 g := fun i ↦ by
      simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using!
            BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
bound : ∀ (i : ℕ), ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i ≤ ↑(nndist 0 g)
⊢ liminf (fun i ↦ (∫⁻ (a : Ω), ENNReal.ofReal (f a) ∂μs i).toReal) atTop =
    (liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop).toReal
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
h,

Goal state after:
case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((Measure.map f μ).prod (Measure.map g μ)) (s ×ˢ t) = (Measure.map f μ) s * (Measure.map g μ) t
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_1.hf
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable Prod.fst (μ.prod ν)

pp: case refine_1.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX =ᵐ[Measure.map Prod.fst (μ.prod ν)] X

Tactic:
· exact measurable_fst.aemeasurable

Goal state after:
case refine_1.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX =ᵐ[Measure.map Prod.fst (μ.prod ν)] X
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 α
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 : ι
hi_mem_union : i ∈ p1 ∪ p2
⊢ g i ∈ s i

Tactic:
Finset.mem_union

Goal state after:
α : 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 : ι
hi_mem_union : i ∈ p1 ∨ i ∈ p2
⊢ g i ∈ 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
⊢ f2 i ∈ s i

Tactic:
exact ht2_m i hi2

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

Goal state before:
pp: case e'_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 : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t) = ((κ.map f ×ₖ κ.map g) ω) (s ×ˢ t)

Tactic:
rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]

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

Goal state before:
pp: ι : 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 μ
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]

Tactic:
cases nonempty_fintype ι
  let g (i' : ι) := if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
  calc
    _ = (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) := by
      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)
    _ = (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) := by
      congr
      calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
    _ = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) := by
      rw [hindep.meas_iInter]
      exact fun i ↦ ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
    _ = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * ∏ i, μ (g i) := by
      rw [hindep.meas_iInter]
      intro i
      by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]
      · obtain ⟨A, hA, hA'⟩ := hf i hi
        exact .inter ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
          ⟨A ×ˢ Set.univ, hA.prod .univ, by ext; simp [← hA']⟩
      · exact ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
    _ = ∏ i, (μ (Y i ⁻¹' t i))⁻¹ * μ (g i) := by
      rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _
    _ = ∏ i, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1 := by
      refine Finset.prod_congr rfl fun i _ ↦ ?_
      by_cases hi : i ∈ s
      · simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]
      · simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top μ _)]
    _ = _ := by simp

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 α
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
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
h_μg : ∀ (n : ι), (κ a) (g n) = (if n ∈ p1 then (κ a) (f1 n) else 1) * if n ∈ p2 then (κ a) (f2 n) else 1
⊢ ∏ n ∈ p1 ∪ p2, (κ a) (g n) = (κ a) t1 * (κ a) t2

Tactic:
h_μg,

Goal state after:
α : 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
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
h_μg : ∀ (n : ι), (κ a) (g n) = (if n ∈ p1 then (κ a) (f1 n) else 1) * if n ∈ p2 then (κ a) (f2 n) else 1
⊢ (∏ x ∈ p1 ∪ p2, (if x ∈ p1 then (κ a) (f1 x) else 1) * if x ∈ p2 then (κ a) (f2 x) else 1) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
⊢ map X ℙ = μ.withDensity (pdf X ℙ μ)

Tactic:
by
  rw [pdf_def, withDensity_rnDeriv_eq _ _ hX.absolutelyContinuous]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ cov[∑ i ∈ s, X i, ∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ AEMeasurable (∑ i ∈ s, X i) μ

Tactic:
covariance_sum_left' (by simpa)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ ∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ MemLp (∑ i ∈ s, X i) 2 μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ AEMeasurable (∑ i ∈ s, X i) μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ = 0
⊢ False

Tactic:
by
    have I : (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.enorm).1 H
    apply h'Y
    filter_upwards [I] with ω hω
    simpa using hω

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (Var[X; μ] / c ^ 2)

Tactic:
by
  rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero hc.ne.symm), hX.ofReal_variance_eq]
  convert! @meas_ge_le_evariance_div_sq _ _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
  · simp
  · rw [ENNReal.ofReal_pow hc.le]
    rfl

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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ Var[∑ i, fun ω ↦ X i (ω i); Measure.pi μ] = ∑ i, Var[X i; μ i]

Tactic:
IndepFun.variance_sum

Goal state after:
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∑ i, Var[fun ω ↦ X i (ω i); Measure.pi μ] = ∑ i, Var[X i; μ i]

case hs
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ i ∈ univ, MemLp (fun ω ↦ X i (ω i)) 2 (Measure.pi μ)

case h
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ).Pairwise fun i j ↦ (fun ω ↦ X i (ω i)) ⟂ᵢ[Measure.pi μ] fun ω ↦ X j (ω j)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
inst✝ : IsProbabilityMeasure P
x : 𝓧
hX : X =ᵐ[P] fun x_1 ↦ x
⊢ HasLaw X (dirac x) P

Tactic:
by
  simpa using hasLaw_smul_dirac_of_ae_eq hX

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
exact ⟨0, fun i => False.elim (hι <| Nonempty.intro i)⟩

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

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ ∏ i, ∫ (x : 𝓧 i), f i x ∂Measure.map (X i) μ = ∏ i, ∫ (ω : Ω), f i (X i ω) ∂μ

pp: case hφ
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEMeasurable (fun ω x ↦ X x ω) μ

pp: case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.map (fun ω x ↦ X x ω) μ)

Tactic:
· congr with i
    rw [integral_map (mX i) (hf i)]

Goal state after:
case hφ
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEMeasurable (fun ω x ↦ X x ω) μ

case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.map (fun ω x ↦ X x ω) μ)
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
F : E → ℝ := fun x ↦ if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
⊢ ∀ (k : ι), (fun x ↦ {x | C ≤ ‖f k x‖}.indicator (fun a ↦ ‖f k a‖) x) = F ∘ f k

Tactic:
intro k

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
F : E → ℝ := fun x ↦ if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
k : ι
⊢ (fun x ↦ {x | C ≤ ‖f k x‖}.indicator (fun a ↦ ‖f k a‖) x) = F ∘ f k
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ f x₁ ∈ s

Tactic:
h,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ f x₂ ∈ s
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
r : ℝ≥0∞
inst✝ : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ μ (s i)
t : Set ℕ
ht : t.Infinite
h : ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s ((Infinite.natEmbedding ι) n))
u : Set ι
hut : u ⊆ ⇑(Infinite.natEmbedding ι) '' t
hu : u.Finite
i : ι
hi : i ∈ u
⊢ ⋂ n ∈ ⇑(Infinite.natEmbedding ι) ⁻¹' u, s ((Infinite.natEmbedding ι) n) ⊆ s i

Tactic:
obtain ⟨n, -, rfl⟩ := hut hi

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
r : ℝ≥0∞
inst✝ : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ μ (s i)
t : Set ℕ
ht : t.Infinite
h : ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s ((Infinite.natEmbedding ι) n))
u : Set ι
hut : u ⊆ ⇑(Infinite.natEmbedding ι) '' t
hu : u.Finite
n : ℕ
hi : (Infinite.natEmbedding ι) n ∈ u
⊢ ⋂ n ∈ ⇑(Infinite.natEmbedding ι) ⁻¹' u, s ((Infinite.natEmbedding ι) n) ⊆ s ((Infinite.natEmbedding ι) n)
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
p : ι → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᵐ[μ] p i
⊢ AEStronglyMeasurable (hs.piecewise f) μ

Tactic:
refine ⟨hs.piecewise p, hs.stronglyMeasurable_piecewise hm hp, ?_⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
p : ι → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᵐ[μ] p i
⊢ hs.piecewise f =ᵐ[μ] hs.piecewise p
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
⊢ mean μ u F univ = 1

Tactic:
refine tendsto_nhds_unique_of_eventuallyEq (hfoel.tendsto_nhds_mean _) tendsto_const_nhds ?_

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
⊢ (fun i ↦ μ (univ ∩ F i) / μ (F i)) =ᶠ[↑u] fun x ↦ 1