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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
have hf_eq_tsum : f = ∑' n, fs n := by
    have h_sum_a : ∀ a, Summable fun n => fs n a :=
      fun _ => Pi.summable.mpr fun _ => ENNReal.summable
    ext a b : 2
    rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a),
      ENNReal.tsum_eq_liminf_sum_nat]
    have h_finsetSum : ∀ n, ∑ i ∈ Finset.range n, fs i a b = min (f a b) n := fun n ↦ by
      induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
    simp_rw [h_finsetSum]
    refine (Filter.Tendsto.liminf_eq ?_).symm
    refine Filter.Tendsto.congr' ?_ tendsto_const_nhds
    rw [Filter.EventuallyEq, Filter.eventually_atTop]
    exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ IsSFiniteKernel (κ.withDensity f)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
k : ℕ
x : (n : ℕ) → X n
h : Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop atBot
⊢ ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)

Tactic:
OrderBot.atBot_eq

Goal state after:
case inl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
k : ℕ
x : (n : ℕ) → X n
h : Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (pure ⊥)
⊢ ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ ∫⁻ (b : γ) in s,
      ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)) ∂(κ + η) a =
    (κ a) s

Tactic:
have hs' : ∀ x ∈ s, rnDerivAux κ (κ + η) a x < 1 := by
    simp_rw [← notMem_mutuallySingularSetSlice]
    exact fun x hx hx_mem ↦ hs hx hx_mem

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
⊢ ∫⁻ (b : γ) in s,
      ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)) ∂(κ + η) a =
    (κ a) s
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = (κ a) s
hκ : ¬(κ a) s = 0
⊢ (κ a) s = 0 ∨ (κ a) s = 1

Tactic:
exact Or.inr <| (ENNReal.mul_eq_left hκ (by simp)).mp this

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
s : Set β
hs : MeasurableSet s
this : f ⁻¹' s = (fun a ↦ (κ a) s) ⁻¹' {1}
⊢ MeasurableSet ((fun a ↦ (κ a) s) ⁻¹' {1})

Tactic:
exact κ.measurable_coe hs <| measurableSet_singleton 1

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ IsMarkovKernel κ†μ

Tactic:
rw [posterior]; infer_instance

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i))
    [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Set ι},
    Countable ↑s →
      ∀ {t : (i : ι) → Set (X i)},
        (∀ i ∈ s, MeasurableSet (t i)) → Nonempty ↑s → (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)
s_ne : ¬Nonempty ↑s
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)

pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)

Tactic:
· simp [Set.not_nonempty_iff_eq_empty'.mp s_ne]

Goal state after:
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    (⇑(Kernel.deterministic f hf) ∘ₘ μ) ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)

Tactic:
rw [Measure.deterministic_comp_eq_map]

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ =
    ((⇑κ ∘ₘ μ) ⊗ₘ κ†μ) (Prod.swap ⁻¹' s ×ˢ t)

Tactic:
Set.preimage_swap_prod,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ =
    ((⇑κ ∘ₘ μ) ⊗ₘ κ†μ) (t ×ˢ s)
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)
inst✝ : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (infinitePi μ) ((↑univ).pi s) = ∏ i, (μ i) (s i)

Tactic:
infinitePi_pi

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ i) (s i) = ∏ i, (μ i) (s i)

case mt
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ i ∈ univ, MeasurableSet (s i)
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)

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

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 y)

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

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

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ geometricPMFReal p n

Tactic:
by
  rw [geometricPMFReal]
  positivity [sub_nonneg.mpr hp_le_one]

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 μ₀
⊢ IsProbabilityMeasure (trajMeasure μ₀ κ)

Tactic:
trajMeasure

Goal state after:
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 μ₀
⊢ IsProbabilityMeasure (⇑(traj κ 0) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ 1 - μ[X | m] = μ[1 | m] - μ[X | m]

Tactic:
simp [Pi.one_def, hm]

Goal state after:
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
f : 𝓨 → 𝓩
hf : Measurable f
⊢ Measure.map (Prod.map id f) (Measure.map X P ⊗ₘ κ) = Measure.map X P ⊗ₘ κ.map f

Tactic:
by rw [Measure.compProd_map hf]

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

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False

Tactic:
map_of_not_aemeasurable h

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
⊢ (if x ∈ t then if x ∈ s then (↑(#s))⁻¹ else 0 else 0) = if x ∈ s ∧ x ∈ t then (↑(#s))⁻¹ else 0

Tactic:
← ite_and,

Goal state after:
α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
⊢ (if x ∈ t ∧ x ∈ s then (↑(#s))⁻¹ else 0) = if x ∈ s ∧ x ∈ t then (↑(#s))⁻¹ else 0
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s.toFinset
⊢ Multiset.count a s = 0

Tactic:
rwa [Multiset.count_eq_zero, ← Multiset.mem_toFinset]

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 μ
ω : Ω
hω : f =ᵐ[(condExpKernel μ m) ω] AEStronglyMeasurable.mk f ⋯
⊢ ∫ (y : Ω), AEStronglyMeasurable.mk f ⋯ y ∂(condExpKernel μ m) ω = ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
rw [integral_congr_ae hω]

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

Goal state before:
pp: case pos
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : μ s = 0
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
rw [Measure.restrict_eq_zero.2 hμs]
    rfl

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 α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ Indep (⨆ n ∈ t, s n) (limsup s f) κ μα

Tactic:
by
  refine indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) ?_
  refine limsSup_le_of_le (by isBoundedDefault) ?_
  simp only [Set.mem_compl_iff, eventually_map]
  exact eventually_of_mem (hf t ht) le_iSup₂

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)

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)

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:
all_goals 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 y ↦ ∏ j, (g j) (y j)) (map (fun c a ↦ Y a c) P)

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:
all_goals 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 x ↦ ∏ i, (f i) (x i)) (map (fun c a ↦ X a c) P)

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:
all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
⊢ ∀ ⦃f : ℕ → X → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f n x ∂π x₀) →
          ∫⁻ (x : X), B.indicator 1 x * (fun x ↦ ⨆ n, f n x) x ∂π x₀ =
            B.indicator 1 x₀ * ∫⁻ (x : X), (fun x ↦ ⨆ n, f n x) x ∂π x₀

Tactic:
rintro f' hf'_meas hf'_mono hf'
    simp_rw [ENNReal.mul_iSup]
    rw [lintegral_iSup (by measurability), lintegral_iSup hf'_meas hf'_mono, ENNReal.mul_iSup]
    · simp_rw [hf']
    · exact hf'_mono.const_mul zero_le

Goal state after: