mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν ν' : Kernel α γ
hνν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x)).toReal ≤
    ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal

Tactic:
have h_le : κ a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x) :=
    meas_countablePartitionSet_le_of_fst_le hκν n a x s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν ν' : Kernel α γ
hνν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x)).toReal ≤
    ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ Submartingale (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)

Tactic:
exact (martingale_densityProcess hκν a hs).submartingale

Goal state after:
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ‖(κ x).real s‖ ≤ κ.bound.toReal

Tactic:
Real.norm_eq_abs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ |(κ x).real s| ≤ κ.bound.toReal
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m ↦ ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 0)

Tactic:
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
  simp_rw [integral_density hκν a (hseq_meas _)]
  rw [← ENNReal.toReal_zero]
  have h_cont := ENNReal.continuousAt_toReal ENNReal.zero_ne_top
  refine h_cont.tendsto.comp ?_
  have h : Tendsto (fun m ↦ κ a (univ ×ˢ seq m)) atTop
      (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n))) := by
    apply tendsto_measure_iInter_atTop
    · measurability
    · exact antitone_const.set_prod hseq
    · exact ⟨0, measure_ne_top _ _⟩
  simpa [← prod_iInter, hseq_iInter] using h

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)

Tactic:
Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),

Goal state after:
case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (η.withDensity (κ.rnDeriv η)) a ≤ κ a

Tactic:
refine Measure.le_intro (fun s hs _ ↦ ?_)

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ ((η.withDensity (κ.rnDeriv η)) a) s ≤ (κ a) s
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
⊢ ∀ (a : α), IsZeroOneMeasure (κ a)

Tactic:
a

Goal state after:
case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
⊢ IsZeroOneMeasure (κ a)
Module: Mathlib.Probability.Kernel.CompProdEqIff

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ η.withDensity (κ.rnDeriv η)) s

Tactic:
Measure.compProd_withDensity,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = ((μ ⊗ₘ η).withDensity fun p ↦ κ.rnDeriv η p.1 p.2) s

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ Measurable (Function.uncurry (κ.rnDeriv η))
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Set ι
s : Finset ↑I
t : (i : ↑I) → Set (X ↑i)
ht : ∀ (i : ↑I), MeasurableSet (t i)
⊢ (map I.domRestrict (infinitePi μ)) ((↑s).pi t) = ∏ i ∈ s, (μ ↑i) (t i)

Tactic:
classical
  rw [map_apply (by fun_prop), domRestrict_preimage, infinitePi_pi _ (by measurability)]
  · simp
  · exact .pi s.countable_toSet (by measurability)

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
| ∫⁻ (θ : Θ), ↑C * ∫⁻ (x : 𝓧), κ.bound ∂P θ ∂π

Tactic:
simp only [lintegral_const, ← mul_assoc]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
| ∫⁻ (θ : Θ), ↑C * κ.bound * (P θ) Set.univ ∂π
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case h
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ ∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂Measure.map (frestrictLe b) ((traj κ a) x₀), Integrable f ((traj κ b) y)

Tactic:
convert! i_f.1
      rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]

Goal state after:
Module: Mathlib.Probability.Distributions.Bernoulli

Goal state before:
pp: case hμ
X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ Integrable f (toNNReal p • dirac x)

pp: case hν
X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ Integrable f (toNNReal (σ p) • dirac y)

Tactic:
all_goals exact (integrable_dirac (by simp)).smul_measure_nnreal

Goal state after:
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ ((geometricMeasure p) {n}).toReal = (1 - ↑p) ^ n * ↑p

Tactic:
geometricMeasure_singleton hp,

Goal state after:
p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal = (1 - ↑p) ^ n * ↑p
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ r * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1

Tactic:
simp [field, ← rpow_add ht]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
⊢ Measure.map (frestrictLe a) (trajMeasure μ₀ κ) ⊗ₘ κ a =
    Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) (trajMeasure μ₀ κ)

Tactic:
rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp _ _ (by fun_prop),
    traj_map_frestrictLe, Measure.comp_assoc, Measure.map_comp _ _ (by fun_prop)]
  congr with x₀ : 1
  rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a

Tactic:
simp only [ENNReal.tsum_eq_zero]
  refine ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => ?_)
  split_ifs with h _ h_1 H h_2
  any_goals ring1
  · absurd H
    simpa [h] using h_1 a'
  · simp [h_2]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h1 : iIndepFun X P
h2 : AEMeasurable (fun ω i ↦ X i ω) P
⊢ map (fun ω i ↦ X i ω) P = infinitePi μ

Tactic:
by
    have := h1.isProbabilityMeasure
    rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀ h2).1 h1]
    simp_rw [fun i ↦ (hX i).map_eq]

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

Goal state before:
pp: case refine_1
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
⊢ iIndepFun (fun i ω x ↦ X i x (ω i x)) (infinitePi fun i ↦ infinitePi (μ i))

Tactic:
exact iIndepFun_infinitePi (P := fun i ↦ infinitePi (μ i))
      (X := fun i u j ↦ X i j (u j)) (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m]

Tactic:
rw [inf_of_le_left hm]

Goal state after:
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f | m ⊓ mΩ] =ᵐ[μ] μ[f | m]

Tactic:
rw [inf_of_le_left hm]

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝¹⁰ : (s : S) → TopologicalSpace (E s)
inst✝⁹ : (s : S) → MeasurableSpace (E s)
inst✝⁸ : ∀ (s : S), BorelSpace (E s)
inst✝⁷ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ AEStronglyMeasurable (fun y ↦ ∏ j, (g j) (y j)) (map (fun c a ↦ Y a c) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝¹⁰ : (s : S) → TopologicalSpace (E s)
inst✝⁹ : (s : S) → MeasurableSpace (E s)
inst✝⁸ : ∀ (s : S), BorelSpace (E s)
inst✝⁷ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, (f i) (x i)) (map (fun c a ↦ X a c) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝¹⁰ : (s : S) → TopologicalSpace (E s)
inst✝⁹ : (s : S) → MeasurableSpace (E s)
inst✝⁸ : ∀ (s : S), BorelSpace (E s)
inst✝⁷ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j))
    (map (fun ω ↦ (fun a ↦ X a ω, fun a ↦ Y a ω)) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα

Tactic:
have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Indep (limsup s atTop) (limsup s atTop) κ μα
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case hfm
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ AEStronglyMeasurable (fun y ↦ ∏ j, (g j) (y j)) (map (fun c a ↦ Y a c) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: case hfm
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ f p.1 * ∏ j, (g j) (p.2 j)) (map (fun ω ↦ (Z ω, fun a ↦ Y a ω)) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = (⇑π ∘ₘ μ) (A ∩ B)

Tactic:
by
  rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable]
  simp only [hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, ← indicator_mul_const, Pi.one_apply, one_mul]
  rw [← lintegral_indicator (h𝓑𝓧 _ hB)]
  rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η₁ : Y₁✝ ⟶ Z₁✝
η₂ : Y₂✝ ⟶ Z₂✝
⊢ ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁ X₂✝ ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝ X₂✝ Y₂✝ κ₂) ≫
      (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) η₁ Y₂✝ ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ Y₂✝ Z₂✝ η₂ =
    (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) (κ₁ ≫ η₁) X₂✝ ≫
      (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ X₂✝ Z₂✝ (κ₂ ≫ η₂)

Tactic:
by
    ext : 1; dsimp
    simp only [Kernel.id_parallelComp_comp_parallelComp_id]
    exact Kernel.parallelComp_comp_parallelComp

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, (f i) (x i)) (map (fun c a ↦ X a c) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ (∏ i, (f i) (p.1 i)) * g p.2) (map (fun ω ↦ (fun a ↦ X a ω, U ω)) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap X.carrier Y.carrier)

Tactic:
by rw [Kernel.swap]; infer_instance

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap Y.carrier X.carrier)

Tactic:
by rw [Kernel.swap]; infer_instance

Goal state after: