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

Goal state before:
pp: case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜ ∩ i ∪ j \ i) = 0

Tactic:
Set.sdiff_eq_compl_inter,

Goal state after:
case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜ ∩ i ∪ iᶜ ∩ j) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (iᶜ \ jᶜ ∪ jᶜ \ iᶜ) = 0

Tactic:
Set.sdiff_eq_compl_inter,

Goal state after:
case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜᶜ ∩ iᶜ ∪ jᶜ \ iᶜ) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜᶜ ∩ iᶜ ∪ jᶜ \ iᶜ) = 0

Tactic:
Set.sdiff_eq_compl_inter,

Goal state after:
case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜᶜ ∩ iᶜ ∪ iᶜᶜ ∩ jᶜ) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ IsFiniteMeasure (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x))

Tactic:
by have := isFiniteMeasure_withDensity_ofReal hfi.neg.2; infer_instance

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (g - f) p μ

Tactic:
simpa [neg_add_eq_sub] using lpNorm_add_le hg.neg (g := g - f) hp

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
x✝ : ∃ y, y.toFiniteMeasure = μ
ν : ProbabilityMeasure Ω
hν : ν.toFiniteMeasure = μ
⊢ μ.mass = 1

Tactic:
by simp [← hν]

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ i ∈ T, s i) = ∑ i ∈ T, μ.restrict (s i)

Tactic:
ext t ht
  simp only [restrict_measure_eq, toMeasure_sum, Measure.coe_finsetSum, Finset.sum_apply]
  rw [Measure.restrict_biUnion_finset hd hm]
  simp only [Measure.sum_fintype, Finset.univ_eq_attach, Measure.coe_finsetSum, Finset.sum_apply]
  conv_rhs => rw [← Finset.sum_attach]

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‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ ENNReal.ofReal δ * ENNReal.ofReal δ⁻¹ * eLpNorm g 1 μ

Tactic:
← ENNReal.ofReal_mul hδ.le,

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
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ ENNReal.ofReal (δ * δ⁻¹) * eLpNorm g 1 μ
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✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
· rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
    rwa [Set.mem_ofPred, hx] at hfx

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : 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
⊢ μ Eᶜ ≤ liminf (fun i ↦ (μs i) Eᶜ) L

Tactic:
rcases L.eq_or_neBot with rfl | hne
  · simp only [liminf_bot, le_top]
  have meas_Ec : μ Eᶜ = 1 - μ E := by
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
  have meas_i_Ec : ∀ i, μs i Eᶜ = 1 - μs i E := by
    intro i
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
  simp_rw [meas_Ec, meas_i_Ec]
  rw [show (L.liminf fun i : ι ↦ 1 - μs i E) = L.liminf ((fun x ↦ 1 - x) ∘ fun i : ι ↦ μs i E)
      from rfl]
  have key := antitone_const_tsub.map_limsup_of_continuousAt (F := L)
    (fun i ↦ μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
  simpa [← key] using antitone_const_tsub h

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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x

pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x

Tactic:
· rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
    rwa [Set.mem_ofPred, hx] at hfx

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ∞
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := ⋯
key₁ : Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ limsup (fun x ↦ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2) L ≤ ↑μ F + ↑ε

Tactic:
rw [limsup_const]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ∞
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
key₁ : Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2 ≤ ↑μ F + ↑ε
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 g : (i : ι) → Ω → β i
hf : iIndepFun f κ μ
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
⊢ iIndepFun g κ μ

Tactic:
iIndepFun_iff_measure_inter_preimage_eq_mul

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 g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, g i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (g i ⁻¹' sets i)
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
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun f κ μ
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ iIndepFun (fun i ↦ g i ∘ f i) κ μ

Tactic:
iIndepFun_iff_measure_inter_preimage_eq_mul

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (γ i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (g i ∘ f i ⁻¹' sets i)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun f μ
this : IsProbabilityMeasure μ
⊢ Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ

Tactic:
iIndepFun_iff_measure_inter_preimage_eq_mul

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
⊢ Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ (Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ) → iIndepFun f μ

Tactic:
iIndepFun_iff_measure_inter_preimage_eq_mul

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ (Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ) →
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
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 : Ω), X x ∂μ) * 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 : Ω), 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 hY.const_mul _ |>.integrable (by simp)

Goal state after:
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 ∂μ) μ

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: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, X; μ] + cov[X, Y; μ] + (cov[Y, X; μ] + cov[Y, Y; μ]) = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
covariance_self,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + cov[X, Y; μ] + (cov[Y, X; μ] + cov[Y, Y; μ]) = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + cov[X, Y; μ] + (cov[Y, X; μ] + cov[Y, Y; μ]) = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
covariance_self,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + cov[X, Y; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable Y μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω ↦ ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False

Tactic:
apply hX

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω ↦ ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp X 2 μ
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 : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
by
  have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
    hf_indep.indepFun_prodMk hf_meas i j k hik hjk
  simpa using! this.comp (measurable_fst.mul measurable_snd) measurable_id

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ iIndepFun (fun n ↦ (s n).indicator fun _ω ↦ 1) κ μ

Tactic:
iIndepFun_iff_measure_inter_preimage_eq_mul

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ,
        (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω ↦ 1) ⁻¹' sets i) =
          ∏ i ∈ S, (κ a) (((s i).indicator fun _ω ↦ 1) ⁻¹' sets i)