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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(- -i)
⊢ x.2 ≤ ↑i

Tactic:
rw [neg_neg] at h'; exact h'.2

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

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst

Tactic:
refine (setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ 0 - 0 = 0

pp: case refine_1.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B (t₀ + t)) P

pp: case refine_1.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B t₀) P

Tactic:
sub_zero

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ 0 = 0

case refine_1.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B (t₀ + t)) P

case refine_1.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B t₀) P
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 : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ |⨅ r, f (a, t) ↑r| ≤ 1

Tactic:
abs_of_nonneg

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ⨅ r, f (a, t) ↑r ≤ 1

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ 0 ≤ ⨅ r, f (a, t) ↑r
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), ((prodMkRight β η) (f ω, b)) (Prod.mk b_1 ⁻¹' s) ∂ξ (f ω, b) =
    ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (f ω, b)

Tactic:
prodMkRight_apply,

Goal state after:
case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), (η (f ω, b).1) (Prod.mk b_1 ⁻¹' s) ∂ξ (f ω, b) =
    ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (f ω, b)
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
⊢ Tendsto
    (fun n ↦
      eLpNorm
        ((fun x ↦ κ.densityProcess ν n a x s) -
          Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a))
        1 (ν a))
    atTop (𝓝 0)

Tactic:
by
  refine Submartingale.tendsto_eLpNorm_one_limitProcess ?_ ?_
  · exact (martingale_densityProcess hκν a hs).submartingale
  · refine uniformIntegrable_of le_rfl ENNReal.one_ne_top ?_ ?_
    · exact fun n ↦ (measurable_densityProcess_right κ ν n a hs).aestronglyMeasurable
    · refine fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩
      · suffices {x | 2 ≤ ‖densityProcess κ ν n a x s‖₊} = ∅ by simp [this]
        ext x
        simp only [mem_ofPred_eq, mem_empty_iff_false, iff_false, not_le]
        refine (?_ : _ ≤ (1 : ℝ≥0)).trans_lt one_lt_two
        rw [Real.nnnorm_of_nonneg (densityProcess_nonneg _ _ _ _ _ _)]
        exact mod_cast (densityProcess_le_one hκν _ _ _ _)
      · simp

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

Goal state before:
pp: case compl
α : 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 γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal - ((κ a) (A ×ˢ s)).toReal

Tactic:
rw [eq_tsub_iff_add_eq_of_le, add_comm]

Goal state after:
case compl
α : 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 γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ((κ a) (A ×ˢ s)).toReal + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal

case compl
α : 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 γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ((κ a) (A ×ˢ s)).toReal ≤ ((κ a) (univ ×ˢ s)).toReal
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 i : ι
⊢ Measurable fun c ↦
    { 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 := ⋯ }
      c i

Tactic:
by_cases hi : i ≤ a

Goal state after:
case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : i ≤ a
⊢ Measurable fun c ↦
    { 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 := ⋯ }
      c i

case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : ¬i ≤ a
⊢ Measurable fun c ↦
    { 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 := ⋯ }
      c i
Module: Mathlib.Probability.Kernel.Disintegration.Density

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

Tactic:
exact ae_of_all _ (fun x m ↦ density_nonneg hκν a x (seq m))

Goal state after:
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 κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a

Tactic:
have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] ∂(κ.withDensity f) a/∂κ a
⊢ (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
this : Function.eval i = Function.eval ⟨i, ⋯⟩ ∘ {i}.restrict
⊢ (map (Function.eval i) (infinitePi μ)) s = (μ i) s

Tactic:
rw [this, ← map_map, infinitePi_map_restrict, (measurePreserving_eval _ _).map_eq]

Goal state after:
case hg
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
this : Function.eval i = Function.eval ⟨i, ⋯⟩ ∘ {i}.restrict
⊢ Measurable (Function.eval ⟨i, ⋯⟩)

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
this : Function.eval i = Function.eval ⟨i, ⋯⟩ ∘ {i}.restrict
⊢ Measurable {i}.restrict
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm)
      (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)

Tactic:
have : (MeasurableEquiv.piCongrLeft (fun _ ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘
        (MeasurableEquiv.curry ι κ X).symm = ⇑(MeasurableEquiv.piCurry (fun _ _ ↦ X)).symm := by
      ext; simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]
    rw [this, infinitePi_map_piCurry_symm]
    convert! infinitePi_map_piCongrLeft (fun p ↦ μ p.1 p.2) (Equiv.sigmaEquivProd ι κ).symm |>.symm

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Countable 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
y : 𝓨
⊢ Measurable fun θ ↦ ℓ θ y * ((κ ∘ₖ P) θ) {y}

Tactic:
exact Measurable.mul (by fun_prop) ((κ ∘ₖ P).measurable_coe (measurableSet_singleton y))

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)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
hf : AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ ∀ᵐ (x : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, AEStronglyMeasurable f ((traj κ b) x)

Tactic:
exact hf.comp

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

Goal state before:
pp: n : ℕ
p : ↑I
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → E
⊢ ∀ i ∈ Finset.Iic n, Integrable f (ENNReal.ofReal (↑(n.choose i) * ↑p ^ i * (1 - ↑p) ^ (n - i)) • dirac i)

Tactic:
exact fun _ _ ↦ (integrable_dirac (by simp)).smul_measure (by simp)

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

Goal state before:
pp: case neg.refine_2.inr.inr.inl
Ω : 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
t : Set Ω
ht : MeasurableSet t
h : t = sᶜ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

pp: case neg.refine_2.inr.inr.inr
Ω : 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
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Tactic:
· simp only [h, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter,
          measureReal_restrict_apply hs.compl, compl_inter_self, measureReal_empty, zero_smul,
          ((Measure.restrict_apply_eq_zero hs.compl).2 <| compl_inter_self s ▸ measure_empty),
          setIntegral_measure_zero]

Goal state after:
case neg.refine_2.inr.inr.inr
Ω : 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
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
condIndepSets_singleton_iff _ _ hs ht

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m'] ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ {
        hom :=
          { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                  inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                  inv_hom_id := ⋯ }.hom.hom ∥ₖ
            Kernel.id,
        property := ⋯ } ≫
      { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        {
          hom :=
            Kernel.id ∥ₖ
              { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                    inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ }.hom.hom,
          property := ⋯ } =
    { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom

Tactic:
ext : 1; dsimp
    simp only [Kernel.id]
    repeat rw [Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)]
    simp [Kernel.deterministic_comp_deterministic]
    rfl

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case pos
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
⊢ μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f n | ↑ℱ i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on (hτ.measurableSpace_le_of_le hτ_le)
      (ℱ.le i) (hτ.measurableSet_eq' i) fun t => ?_

Goal state after:
case pos
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
t : Set Ω
⊢ MeasurableSet ({x | τ x = ↑i} ∩ t) ↔ MeasurableSet ({x | τ x = ↑i} ∩ t)
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})

Tactic:
hτ.measurableSet_inter_le_iff hσ,

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e_f
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h :
  Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.deterministic id ⋯ ×ₖ condDistrib g k μ) =
    Kernel.id ∘ₖ (Kernel.deterministic id ⋯ ×ₖ condDistrib g k μ) ×ₖ (condDistrib f k μ ∘ₖ Kernel.deterministic id ⋯)
⊢ Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
    Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ)

Tactic:
← Kernel.id

Goal state after:
case e_f
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h :
  Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ) =
    Kernel.id ∘ₖ (Kernel.id ×ₖ condDistrib g k μ) ×ₖ (condDistrib f k μ ∘ₖ Kernel.id)
⊢ Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
    Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ)
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf' hs, exp_sub]

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)