mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
by
  by_cases! hm : ¬ m ≤ m0
  · simpa [condExp_of_not_le hm] using integral_nonneg (fun x => abs_nonneg f x)
  by_cases! hfint : ¬ Integrable f μ
  · simpa [condExp_of_not_integrable hfint] using integral_nonneg (fun x => abs_nonneg f x)
  by_cases! hsig : ¬ SigmaFinite (μ.trim hm)
  · simpa [condExp_of_not_sigmaFinite hm hsig] using integral_nonneg (fun x => abs_nonneg f x)
  calc
  _ = ∫ x in s, |(μ.restrict s)[f | m] x| ∂μ :=
    (integral_congr_ae ((condExp_restrict_ae_eq_restrict hm hs hfint).fun_comp abs)).symm
  _  ≤ _ := integral_abs_condExp_le f

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
μ : ProbabilityMeasure Ω
f : ι → Set Ω
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
simpa [← ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.tendsto_coe]
    using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure)

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this : ↑μ (s₁ ∪ s₂) ≤ ↑μ s₁ + ↑μ s₂
⊢ ↑μ s₁ + ↑μ s₂ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this : ↑μ (s₁ ∪ s₂) ≤ ↑μ s₁ + ↑μ s₂
⊢ ↑μ s₁ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this : ↑μ (s₁ ∪ s₂) ≤ ↑μ s₁ + ↑μ s₂
⊢ ↑μ s₂ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ = μ.mass • μ.normalize.toFiniteMeasure

Tactic:
by
  apply eq_of_forall_apply_eq
  intro s _s_mble
  rw [μ.self_eq_mass_mul_normalize s, smul_apply, smul_eq_mul,
    ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn]

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

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun i ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds

Goal state after:
case neg
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (ProbabilityMeasure.toFiniteMeasure ∘ fun i ↦ (μs i).normalize) F (𝓝 μ.normalize.toFiniteMeasure)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun i ↦ (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
    (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ↑C * μ univ ^ p.toReal⁻¹ + 1 ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ μ (f ⁻¹' (f '' K)ᶜ) ≤ ε

Tactic:
refine (measure_mono ?_).trans (hKS μ hμS)

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ f ⁻¹' (f '' K)ᶜ ⊆ Kᶜ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s t : Set Ω
⊢ IndepSet s t κ 0

Tactic:
simp [IndepSet]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
⊢ IndepSet s t 0 μ

Tactic:
simp [IndepSet]

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i ↦ (μs i) E₀) L
h_E₁ : limsup (fun i ↦ (μs i) E₁) L ≤ μ E₁
⊢ Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))

Tactic:
apply tendsto_of_le_liminf_of_limsup_le

Goal state after:
case hinf
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i ↦ (μs i) E₀) L
h_E₁ : limsup (fun i ↦ (μs i) E₁) L ≤ μ E₁
⊢ μ E ≤ liminf (fun i ↦ (μs i) E) L

case hsup
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i ↦ (μs i) E₀) L
h_E₁ : limsup (fun i ↦ (μs i) E₁) L ≤ μ E₁
⊢ limsup (fun i ↦ (μs i) E) L ≤ μ E

case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i ↦ (μs i) E₀) L
h_E₁ : limsup (fun i ↦ (μs i) E₁) L ≤ μ E₁
⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ (μs i) E) tendsto_of_le_liminf_of_limsup_le._auto_1

case h'
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i ↦ (μs i) E₀) L
h_E₁ : limsup (fun i ↦ (μs i) E₁) L ≤ μ E₁
⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) L fun i ↦ (μs i) E) tendsto_of_le_liminf_of_limsup_le._auto_3
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simp only [iIndep_iff_iIndepSets, iIndepSets_iff]; rfl

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s μ ↔
    ∀ (s' : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s', MeasurableSet (f i)) → μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i)

Tactic:
simp only [iIndepSet_iff_iIndep, iIndep_iff]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable f (⇑κ ∘ₘ μ)
hg : AEMeasurable g (⇑κ ∘ₘ μ)
hφ : AEMeasurable φ (Measure.map f (⇑κ ∘ₘ μ))
hψ : AEMeasurable ψ (Measure.map g (⇑κ ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
⊢ (∀ᵐ (ω : Ω) ∂κ a, φ (f ω) = AEMeasurable.mk φ hφ (f ω)) → AEMeasurable.mk φ hφ ∘ f =ᵐ[κ a] φ ∘ f

Tactic:
haφ

Goal state after:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable f (⇑κ ∘ₘ μ)
hg : AEMeasurable g (⇑κ ∘ₘ μ)
hφ : AEMeasurable φ (Measure.map f (⇑κ ∘ₘ μ))
hψ : AEMeasurable ψ (Measure.map g (⇑κ ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haφ : ∀ᵐ (ω : Ω) ∂κ a, φ (f ω) = AEMeasurable.mk φ hφ (f ω)
⊢ AEMeasurable.mk φ hφ ∘ f =ᵐ[κ a] φ ∘ f
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 μ
⊢ Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ

Tactic:
have := h.isProbabilityMeasure
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
    constructor
    · congr with x
      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp
  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
  rw [← (h₀ hm).1, ← (h₀ hm).2]
  simpa [hm] using h Finset.univ (sets := h')

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

Goal state before:
pp: case refine_2
α : 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 : (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

Tactic:
rw [Measure.ext_prod₃_iff] at h

Goal state after:
case refine_2
α : 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
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (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:
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.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 μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ ∏ i, (μ (Y i ⁻¹' t i))⁻¹ * μ (g i) = ∏ i, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1

Tactic:
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 μ _)]

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
⊢ IsOpen[inst✝³] G → ν G ≤ liminf (fun i ↦ (μ i) G) l

Tactic:
hG

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
⊢ ν G ≤ liminf (fun i ↦ (μ i) G) l
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case refine_1.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), f n ∈ {s | MeasurableSet s}
⊢ ⋃ i, f i ∈ {s | MeasurableSet s}

Tactic:
exact .iUnion hf

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

Goal state before:
pp: case refine_2.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
f : ℕ → Set Ω
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), f n ∈ {s | MeasurableSet s}
⊢ ⋃ i, f i ∈ {s | MeasurableSet s}

Tactic:
exact .iUnion hf

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

Goal state before:
pp: case iSup
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ⨆ n, ∫⁻ (a : Ω), f a * f' n a ∂μ = ⨆ i, (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ

Tactic:
simp_rw [← h_ind_f']

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ ∫ (ω : Ω), (X ω + Y ω - ∫ (x : Ω), X x + Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ) ∂μ =
    ∫ (a : Ω),
      (X a - ∫ (x : Ω), X x ∂μ) * (Z a - ∫ (x : Ω), Z x ∂μ) + (Y a - ∫ (x : Ω), Y x ∂μ) * (Z a - ∫ (x : Ω), Z x ∂μ) ∂μ

Tactic:
congr with x
    rw [integral_add (hX.integrable (by simp)) (hY.integrable (by simp))]
    ring

Goal state after:
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✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousENorm F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ ↑C * ‖x‖ₑ * ‖y‖ₑ
⊢ ↑C < ∞

Tactic:
finiteness

Goal state after:
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
𝕜 : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖(B x) y‖ₑ ≠ ∞

Tactic:
finiteness

Goal state after:
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
𝕜 : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ↑‖B‖₊ * ‖x‖ₑ * ‖y‖ₑ ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
⊢ IsProbabilityMeasure P ↔ IsProbabilityMeasure (map X P)

Tactic:
isProbabilityMeasure_map_iff hX.aemeasurable

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
⊢ IsProbabilityMeasure P ↔ IsProbabilityMeasure P
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case ha
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
x : E
y : F
⊢ ↑c * ‖x‖ₑ * ‖y‖ₑ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: case hb
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
x : E
y : F
⊢ ‖(B x) y‖ₑ ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[inst✝²] t

Tactic:
filter_upwards [ht] with x hx using subset_closure hx

Goal state after: