mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ m v, Measure.map (⇑L) μ = gaussianReal m v
⊢ IsGaussian μ

Tactic:
refine isGaussian_of_isGaussian_map fun L ↦ ?_
  obtain ⟨m, v, h⟩ := h L
  rw [h]
  infer_instance

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

Goal state before:
pp: case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ Integrable (fun x ↦ x) μ

Tactic:
exact h.integrable (by simp)

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

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L : StrongDual ℝ E
h : MemLp id 2 μ
⊢ 0 ≤
    inner ℝ ((StrongDual.toLp (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) 2) L)
      ((StrongDual.toLp (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) 2) L)

Tactic:
exact real_inner_self_nonneg

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ Var[fun x ↦ x s; projectiveFamily I] = ↑↑s

Tactic:
rw [← covariance_self, covariance_eval_projectiveFamily, min_self]
  exact aemeasurable_id.eval s

Goal state after:
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: case refine_2
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h :
  ∀ (I : Finset T), Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
· have hX' := isProjectiveLimit_map hX
    simp_rw [h] at hX'
    exact hX'.unique (isProjectiveLimit_map hY)

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁶ : LinearOrder T
inst✝⁵ : Bot T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
⊢ (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P]
    ⇑(incrementsToRestrict R I) ∘ fun ω i ↦
      X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω

Tactic:
filter_upwards [h] with ω hω
  ext t
  simp only [restrict, incrementsToRestrict, ContinuousLinearMap.coe_mk', LinearMap.coe_mk,
    AddHom.coe_mk, Function.comp_apply]
  rw [Fin.sum_Iic_sub _ (fun j ↦ X (I.orderEmbOfFinWithBot j) ω)]
  simp [hω, orderEmbOfFin]

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: case inr
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this✝ : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P]
    ⇑(incrementsToRestrict ℝ I) ∘ fun ω i ↦
      X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω
i : Fin #I
⊢ X (I.orderEmbOfFinWithBot i.castSucc) ⟂ᵢ[P] X (I.orderEmbOfFinWithBot i.succ) - X (I.orderEmbOfFinWithBot i.castSucc)

Tactic:
exact incr.indepFun_eval_sub bot_le
      (monotone_orderEmbOfFinWithBot I (Fin.castSucc_le_succ i)) h_bot

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: q : ℚ
⊢ (if q < 0 then 0 else 1) ≤ 1

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P] =
    ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; projectiveFamily I]

Tactic:
congrm ∑ i, ∑ j, _ * ?_

Goal state after:
case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
⊢ cov[fun ω ↦ ω i, fun ω ↦ ω j; Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P] =
    cov[fun ω ↦ ω i, fun ω ↦ ω j; projectiveFamily I]
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Tactic:
have h_exists : ∀ x : ℝ, ∃ q : ℚ, x - 1 < q ∧ ↑q < x := fun x ↦ exists_rat_btwn (sub_one_lt x)

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
h : i < j
h1 : i.succ ≤ j.succ
h2 : i.castSucc ≤ j.succ
h3 : i.castSucc ≤ j.castSucc
⊢ ↑(t i.succ) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    0

Tactic:
min_eq_left (ht h),

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
h : i < j
h1 : i.succ ≤ j.succ
h2 : i.castSucc ≤ j.succ
h3 : i.castSucc ≤ j.castSucc
⊢ ↑(t i.succ) - ↑(t i.succ) - ↑(min (t i.castSucc) (t j.succ)) + ↑(min (t i.castSucc) (t j.castSucc)) = 0
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ Integrable id (Measure.map X P)

Tactic:
exact hX.isGaussian_map.integrable_id

Goal state after:
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 : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ mγ = generateFrom {s | ∃ n, MeasurableSet s}

Tactic:
ofPred_exists,

Goal state after:
α : 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
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ mγ = generateFrom (⋃ i, {x | MeasurableSet x})
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)

Tactic:
integrable_map_measure hf (hX.aemeasurable.prodMk hY)

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable (f ∘ fun a ↦ (X a, Y a)) μ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ.fst a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)))

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0 ⊢
    suffices ∀ m, κ a (countablePartitionSet n x ×ˢ seq m) = 0 by
      simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]
      suffices κ a (countablePartitionSet n x ×ˢ univ) = 0 by
        simp only [this, ENNReal.zero_div]
      convert! h0
      ext x
      simp only [mem_prod, mem_univ, and_true, mem_ofPred_eq]
    refine fun m ↦ measure_mono_null (fun x ↦ ?_) h0
    simp only [mem_prod, mem_ofPred_eq, and_imp]
    exact fun h _ ↦ h

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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ (trajContent κ (frestrictLe a x₀)) (cylinder (Iic b) S) =
    lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x₀

Tactic:
rw [trajContent_cylinder mS, ← lintegral_indicator_one mS, lmarginalPartialTraj]
  congr with x
  apply Set.indicator_const_eq_indicator_const
  rw [mem_cylinder]
  congrm (fun i ↦ ?_) ∈ S
  simp [updateFinset, i.2]

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)
⊢ κ.withDensity (f + g) = κ.withDensity f + κ.withDensity g

Tactic:
ext a
  rw [add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg,
    Kernel.withDensity_apply, Pi.add_apply, MeasureTheory.withDensity_add_right]
  · fun_prop
  · exact hf.add hg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ ∫⁻ (b : β) in Set.univ, f a b ∂κ a ≤ B * κ.bound

Tactic:
calc
          ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
          _ = B * κ a Set.univ := by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
          _ ≤ B * κ.bound := by grw [measure_le_bound]

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

Goal state before:
pp: α : 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
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
⊢ f = ∑' (n : ℕ), fs n

Tactic:
ext a b : 2

Goal state after:
α : 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
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
⊢ f a b = (∑' (n : ℕ), fs n) a b
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 : α
⊢ ∀ᵐ (x : γ) ∂((κ + η) a).restrict {x | 1 ≤ κ.rnDerivAux (κ + η) a x},
    ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable fun b ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)

pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry fun a x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))

Tactic:
ae_restrict_iff

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a, x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} → ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ MeasurableSet {x | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable fun b ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)

case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry fun a x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂((κ + η) a).restrict (κ.mutuallySingularSetSlice η a)ᶜ,
    ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun b ↦ ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b

pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x ↦
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)

Tactic:
ae_restrict_iff

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a,
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ MeasurableSet
    {x | ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x}

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun b ↦ ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b

case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x ↦
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj κ a b f x₀ = f x₀

Tactic:
rw [lmarginalPartialTraj, partialTraj_le hba, Kernel.lintegral_deterministic']

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ f (updateFinset x₀ (Iic b) (frestrictLe₂ hba (frestrictLe a x₀))) = f x₀

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable fun z ↦ f (updateFinset x₀ (Iic b) 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 ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
let s := κ.mutuallySingularSet η

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 η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
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 Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
⊢ μ ⊗ₘ κ ≪ μ.prod ν

Tactic:
rw [← Measure.compProd_const]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ν
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 : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
⊢ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ

Tactic:
rw [← Measure.compProd_const]

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 : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
⊢ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ) ⊗ₘ Kernel.const 𝓧 μ
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ avgRisk ℓ P κ π = ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π

Tactic:
rw [avgRisk, ← Measure.lintegral_compProd (f := fun θy ↦ ℓ θy.1 θy.2) (by fun_prop)]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (x : Θ × 𝓨), ℓ x.1 x.2 ∂π ⊗ₘ (κ ∘ₖ P) = ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (a : ℝ) in Ioo 0 1, 1 / beta α β * (a ^ (α - 1) * (1 - a) ^ (β - 1)) = 1

Tactic:
integral_const_mul

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 1 / beta α β * ∫ (a : ℝ) in Ioo 0 1, a ^ (α - 1) * (1 - a) ^ (β - 1) = 1