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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ * 1))

Tactic:
mul_one

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ))
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] ≤ᵐ[μ] μ[X ^ 2 | m]

Tactic:
filter_upwards [condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX] with ω hω
  dsimp at hω
  nlinarith

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 =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
· rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),
      restrict₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᵐ[κ a] g a
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a).withDensity (f a)) s✝ = ((κ.withDensity g) a) s✝

Tactic:
Kernel.withDensity_apply _ hg,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᵐ[κ a] g a
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a).withDensity (f a)) s✝ = ((κ a).withDensity (g a)) s✝
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity (f + g)) a) s✝ = ((κ a).withDensity (f a) + (κ.withDensity g) a) s✝

Tactic:
Kernel.withDensity_apply _ hg,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity (f + g)) a) s✝ = ((κ a).withDensity (f a) + (κ a).withDensity (g a)) s✝
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
⊢ partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b =
    (Kernel.id ×ₖ const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)).map (_root_.IicProdIoc a b)

Tactic:
by
  rw [partialTraj_eq_prod, partialTraj_const_restrict₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ (((κ a).withDensity fun x ↦ ↑(f a x)).withDensity fun x ↦ g a x) =
    ((κ.withDensity fun a x ↦ ↑(f a x)).withDensity g) a

Tactic:
Kernel.withDensity_apply _ hg,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ (((κ a).withDensity fun x ↦ ↑(f a x)).withDensity fun x ↦ g a x) =
    ((κ.withDensity fun a x ↦ ↑(f a x)) a).withDensity (g a)
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 η
hκη : κ ≤ η
a : α
⊢ κ.rnDerivAux η a ≤ᵐ[η a] 1

Tactic:
by
  filter_upwards [Measure.rnDeriv_le_one_of_le (hκη a)] with x hx_le_one
  simp_rw [rnDerivAux]
  split_ifs with hα
  · refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
    simp only [Pi.one_apply, ENNReal.ofReal_one]
    exact hx_le_one
  · have := hαγ.countableOrCountablyGenerated.resolve_left hα
    exact density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

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

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((κ.map fun a ↦ (a, ())).density (κ + η) a x univ) ∂(κ + η) a = (κ a) s

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left hα
    rw [setLIntegral_density ((fst_map_id_prod _ measurable_const).trans_le h_le) _
      MeasurableSet.univ hs, map_apply' _ (by fun_prop) _ (hs.prod MeasurableSet.univ)]
    congr 1 with x
    simp

Goal state after:
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 η
h_le : κ ≤ κ + η
⊢ (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η

Tactic:
ofNNReal_toNNReal,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ (((κ + η).withDensity fun a x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun a x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η
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 η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)

Tactic:
ofNNReal_toNNReal,

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
x : γ
hx : x ∈ s
⊢ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj κ a (a + 1) f x₀ = ∫⁻ (x : X (a + 1)), f (update x₀ (a + 1) x) ∂(κ a) (frestrictLe a x₀)

Tactic:
rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset x₀ (Iic (a + 1))
          (_root_.IicProdIoc a (a + 1) (frestrictLe a x₀, (piSingleton a) a_1))) ∂(κ a) (frestrictLe a x₀) =
    ∫⁻ (x : X (a + 1)), f (update x₀ (a + 1) x) ∂(κ a) (frestrictLe a x₀)

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable ⇑(piSingleton a)

case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable fun b ↦ f (updateFinset x₀ (Iic (a + 1)) (_root_.IicProdIoc a (a + 1) (frestrictLe a x₀, b)))

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable fun a_1 ↦ f (updateFinset x₀ (Iic (a + 1)) (_root_.IicProdIoc a (a + 1) a_1))

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (_root_.IicProdIoc a (a + 1))

case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable fun z ↦ f (updateFinset x₀ (Iic (a + 1)) z)
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧ (μ ⊗ₘ κ) sᶜ = 0

Tactic:
compProd_apply hs.compl

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
⊢ ∃ f, ∃ (hf : Measurable f), κ = deterministic f hf

Tactic:
choose f hf using fun a ↦ exists_eq_dirac (μ := κ a)

Goal state after:
α : 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)
⊢ ∃ f, ∃ (hf : Measurable f), κ = deterministic f hf
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : MeasurableSpace R
inst✝¹ : AddMonoidWithOne R
inst✝ : MeasurableSingletonClass R
n : ℕ
p : ↑I
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.Iic n
⊢ map Nat.cast (ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac x✝¹) =
    ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac ↑x✝¹

Tactic:
by rw [Measure.map_smul, map_dirac]

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

Goal state before:
pp: α : Type u_1
p : PMF α
⊢ p.toOuterMeasure.caratheodory = ⊤

Tactic:
refine eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)
  have ⟨y, hy⟩ := hx
  exact
    ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p = μ.toPMF

Tactic:
← toMeasure_inj,

Goal state after:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p.toMeasure = μ.toPMF.toMeasure
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toPMF = p ↔ μ = p.toMeasure

Tactic:
← toMeasure_inj,

Goal state after:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toPMF.toMeasure = p.toMeasure ↔ μ = p.toMeasure
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < Po(r).real {n}

Tactic:
rw [poissonMeasure_real_singleton]
  positivity

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

Goal state before:
pp: α : Type u_1
p : PMF α
x : α
⊢ p x * 1 = p x

Tactic:
mul_one

Goal state after:
α : Type u_1
p : PMF α
x : α
⊢ p x = p x
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : ¬p a = 0
⊢ p a * 1 = p a

Tactic:
mul_one

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : ¬p a = 0
⊢ p a = p a
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case true
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_ofPred_eq, ne_eq,
      ENNReal.coe_eq_zero]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
· simp [pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inr hnt), hnt]

Goal state after:
case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

Tactic:
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hnt.1 hnt.2 huX

Goal state after:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s))) / ↑s.card

Tactic:
by
  simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
  refine tsum_congr fun x => ?_
  by_cases hx : x ∈ t <;> simp [Set.indicator, hx, div_eq_mul_inv]

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
hf_int : Integrable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((condExpKernel μ m) ω)

Tactic:
by
  nontriviality Ω
  rw [condExpKernel_eq]
  convert!
    Integrable.condDistrib_ae (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
      hf_int.comp_snd_map_prod_id using 1

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
hf_int : Integrable f μ
⊢ Integrable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
by
  nontriviality Ω
  rw [condExpKernel_eq]
  convert!
    Integrable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ))
      aemeasurable_id hf_int.comp_snd_map_prod_id using 1

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
by
  have : (fun ω ↦ (condExpKernel μ (generateFrom {s}) ω).real t) =ᵐ[μ.restrict s]
      μ⟦t | generateFrom {s}⟧ :=
    ae_restrict_le <| condExpKernel_ae_eq_condExp
      (generateFrom_singleton_le hs) ht
  filter_upwards [condExp_set_generateFrom_singleton hs ht, this] with ω hω₁ hω₂
  rwa [hω₁, measureReal_def, measureReal_def,
    ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃A : Set X⦄,
      MeasurableSet A →
        ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]

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

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯