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

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * a ^ 2)) ∂μ

Tactic:
refine setLIntegral_mono (by fun_prop) fun x hx ↦ ?_
      gcongr
      · exact mul_nonneg (logRatio_nonneg hc'_gt.le hc'_le) (by positivity)
      · simpa using hx

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
        ∏ i, charFunDual (Measure.map (X i) P) (L ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by
  rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
refine (lintegral_exp_mul_sq_norm_le_mul h_rot ha_pos hc hc_gt).trans ?_

Goal state after:
case inr
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
⊢ μ {x | ‖x‖ ≤ a} *
      (ENNReal.ofReal (rexp (logRatio c)) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))) ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a

Tactic:
congr with b : 1

Goal state after:
case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) =
    ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ((ν a).restrict s)

Tactic:
exact (integrable_stieltjesOfMeasurableRat hf _ _).restrict

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
filter_upwards [this] with t ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (⋃ i, f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)

Tactic:
| iUnion f hf_disj hf_meas ihf =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂ν a✝ =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) t₂ ∂ν a✝
a : β
hat₁ : a ∉ t₁
⊢ ((IsCondKernelCDF.toKernel f hf) (a✝, a)) (Prod.mk a ⁻¹' t₁ ×ˢ t₂) = 0

Tactic:
simp only [hat₁, not_false_eq_true, mk_preimage_prod_right_eq_empty, measure_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
this : Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅
⊢ (κ a) (Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ) = 0

Tactic:
rw [this]; simp

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a : ι
⊢ Measurable
    ⇑{ toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }

Tactic:
by
    refine measurable_pi_lambda _ (fun i ↦ ?_)
    by_cases hi : i ≤ a <;> simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]
    · exact measurable_fst.eval
    · exact measurable_snd.eval

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

Goal state before:
pp: case e'_5
α : 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 : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ univ = ⋃ n, univ ×ˢ seq n

Tactic:
rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]

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

Goal state before:
pp: case refine_2
α : 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_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ∞ → ∫ (x : α) in s, ∫ (y : Ω), f (X x, y) ∂(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in s, f (X x, Y x) ∂μ

Tactic:
rintro s ⟨t, ht, rfl⟩ _
    change ∫ a in X ⁻¹' t, ((fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x') ∘ X) a ∂μ =
      ∫ a in X ⁻¹' t, f (X a, Y a) ∂μ
    simp only [Function.comp_apply]
    rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]
    swap
    · rw [← Measure.restrict_map hX ht]
      exact (hf_int.1.integral_condDistrib_map hY).restrict
    rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
      Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
      setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),
      mk_preimage_prod, preimage_univ, inter_univ]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x

Tactic:
· rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]

Goal state after:
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
⊢ G(V, p) {G} = ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
by
  classical
  cases nonempty_fintype V
  simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
  rw [Set.ncard_sdiff (by simp)]
  congr!
  rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]

Goal state after:
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 : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (Measure.pi fun i ↦ μ ↑i)
      (⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }) ⁻¹' s) =
    (Measure.pi μ) s

Tactic:
← Measure.pi_map_piCongrLeft e,

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 : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (Measure.pi fun i ↦ μ ↑i)
      (⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }) ⁻¹' s) =
    (Measure.map (⇑(piCongrLeft (fun i ↦ X i) e)) (Measure.pi fun i ↦ μ (e i))) s
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ (map (⇑(piSingleton n)) (μ (n + 1))) (Set.univ.pi s) = ∏ i, (μ ↑i) (s i)

Tactic:
Fintype.prod_subsingleton _ ⟨n + 1, mem_Ioc.2 (by lia)⟩,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ (map (⇑(piSingleton n)) (μ (n + 1))) (Set.univ.pi s) = (μ ↑⟨n + 1, ⋯⟩) (s ⟨n + 1, ⋯⟩)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
h_eq_sum : κ.withDensity f = Kernel.sum fun i ↦ (κ.seq i).withDensity f
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [h_eq_sum]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
h_eq_sum : κ.withDensity f = Kernel.sum fun i ↦ (κ.seq i).withDensity f
⊢ IsSFiniteKernel (Kernel.sum fun i ↦ (κ.seq i).withDensity f)
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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (infinitePiNat fun n ↦ μ (e n)) (I.restrict ∘ ⇑(piCongrLeft X e) ⁻¹' S) = (piContent μ) (I.restrict ⁻¹' S)

pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)

Tactic:
coe_piCongrLeft,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (infinitePiNat fun n ↦ μ (e n)) (I.restrict ∘ ⇑(Equiv.piCongrLeft X e) ⁻¹' S) = (piContent μ) (I.restrict ⁻¹' S)

ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)
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 : α
⊢ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq,
    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.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:
rw [ofNNReal_toNNReal, ← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul,
        ← mul_assoc, mul_inv_cancel₀, one_mul]

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
⊢ 1 - κ.rnDerivAux (κ + η) a x ≠ 0

α : 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
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

α : 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
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x
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 : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ (κ a) s = 0 ∨ (κ a) s = 1

Tactic:
copy_comp_apply_prod,

Goal state after:
case mp
α : 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 ∩ s)
⊢ (κ a) s = 0 ∨ (κ a) s = 1

case mp.hs
α : 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 = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s

case mp.ht
α : 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 = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ μ (e i)) (⇑(piCongrLeft X e) ⁻¹' (⇑e '' ↑(s.preimage ⇑e ⋯)).pi t) = ∏ i ∈ s, (μ i) (t i)

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable ⇑(piCongrLeft X e)

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ MeasurableSet ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t)

Tactic:
coe_piCongrLeft,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ μ (e i)) (⇑(Equiv.piCongrLeft X e) ⁻¹' (⇑e '' ↑(s.preimage ⇑e ⋯)).pi t) = ∏ i ∈ s, (μ i) (t i)

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable ⇑(piCongrLeft X e)

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ MeasurableSet ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t)
Module: Mathlib.Probability.Distributions.Beta

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

Tactic:
div_eq_one_iff_eq (ne_of_gt (beta_pos hα hβ)),

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (a : ℝ) in Ioo 0 1, a ^ (α - 1) * (1 - a) ^ (β - 1) = beta α β
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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ a) x₀)
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i), ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (x : (n : ℕ) → X n), f x ∂(traj κ a) x₀

Tactic:
apply integral_traj_partialTraj' hab
  rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
  exact hf.comp_measurable measurable_snd

Goal state after: