mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun ω s ↦ X s ω

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ MemLp X (↑p) (μ.tilted fun x ↦ t * X x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
s : S
⊢ Continuous (Function.eval s)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')

Tactic:
by

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

Goal state before:
pp: Ω : 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_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ ↑p ≠ ∞

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Var[X; μ.tilted fun x ↦ t * X x] = iteratedDeriv 2 (cgf X μ) t

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun ω s ↦ X s ω

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∑ a, ↑(p ^ ↑a * (1 - p) ^ (↑(Fin.last n) - ↑a) * ↑(n.choose ↑a)) = 1

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
i : Fin (n + 1)
⊢ (binomial p h n) i = ↑p ^ ↑i * (1 - ↑p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) 0 = (1 - ↑p) ^ n

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) (Fin.last n) = ↑p ^ n

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ rexp (t * X ω)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] Z

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ rexp (↑p * t * X ω)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : (t : T) → TopologicalSpace (F t)
inst✝³ : (t : T) → MeasurableSpace (F t)
inst✝² : ∀ (t : T), BorelSpace (F t)
inst✝¹ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : (s : ↥I) → E ↑s →ᵇ ℝ) (g : (t : ↥J) → F ↑t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P
I : Finset S
J : Finset T
⊢ ∀ (s : ↥I), AEMeasurable (X ↑s) P

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
⊢ binomial p h 1 = map (fun x ↦ bif x then 1 else 0) (bernoulli p h)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : (t : T) → TopologicalSpace (F t)
inst✝³ : (t : T) → MeasurableSpace (F t)
inst✝² : ∀ (t : T), BorelSpace (F t)
inst✝¹ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : (s : ↥I) → E ↑s →ᵇ ℝ) (g : (t : ↥J) → F ↑t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P
I : Finset S
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (Y ↑t) P

Tactic:
by

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
⊢ k % (b + 1) = k

Tactic:
by

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
⊢ 1 - ↑x = ENNReal.ofReal (1 - ↑x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : (t : T) → TopologicalSpace (F t)
inst✝³ : (t : T) → MeasurableSpace (F t)
inst✝² : ∀ (t : T), BorelSpace (F t)
inst✝¹ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : ((s : ↥I) → E ↑s) →ᵇ ℝ) (g : ((t : ↥J) → F ↑t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X (↑x) ω) * g fun x ↦ Y (↑x) ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X (↑x) ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y (↑x) ω) x ∂P
I : Finset S
J : Finset T
⊢ ∀ (s : ↥I), AEMeasurable (X ↑s) P

Tactic:
by

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
⊢ 1 - ↑x ≥ 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : (t : T) → TopologicalSpace (F t)
inst✝³ : (t : T) → MeasurableSpace (F t)
inst✝² : ∀ (t : T), BorelSpace (F t)
inst✝¹ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : ((s : ↥I) → E ↑s) →ᵇ ℝ) (g : ((t : ↥J) → F ↑t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X (↑x) ω) * g fun x ↦ Y (↑x) ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X (↑x) ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y (↑x) ω) x ∂P
I : Finset S
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (Y ↑t) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁸ : (t : T) → TopologicalSpace (F t)
inst✝⁷ : (t : T) → MeasurableSpace (F t)
inst✝⁶ : ∀ (t : T), BorelSpace (F t)
inst✝⁵ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝ : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : (t : ↥J) → F ↑t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P
J : Finset T
⊢ AEMeasurable Z P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁸ : (t : T) → TopologicalSpace (F t)
inst✝⁷ : (t : T) → MeasurableSpace (F t)
inst✝⁶ : ∀ (t : T), BorelSpace (F t)
inst✝⁵ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝ : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : (t : ↥J) → F ↑t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (Y ↑t) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁸ : (t : T) → TopologicalSpace (F t)
inst✝⁷ : (t : T) → MeasurableSpace (F t)
inst✝⁶ : ∀ (t : T), BorelSpace (F t)
inst✝⁵ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝ : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : ((t : ↥J) → F ↑t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y (↑x) ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y (↑x) ω) x ∂P
J : Finset T
⊢ AEMeasurable Z P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁸ : (t : T) → TopologicalSpace (F t)
inst✝⁷ : (t : T) → MeasurableSpace (F t)
inst✝⁶ : ∀ (t : T), BorelSpace (F t)
inst✝⁵ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝ : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : ((t : ↥J) → F ↑t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y (↑x) ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y (↑x) ω) x ∂P
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (Y ↑t) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : (s : ↥I) → E ↑s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (X ↑s) P

Tactic:
by

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

Goal state before:
pp: Ω : 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_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
h :
  Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ = ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ
⊢ Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ) =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : (s : ↥I) → E ↑s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
I : Finset S
⊢ AEMeasurable U P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : κ ω' = 0
⊢ 0 ≤ ↑c * t ^ 2 / 2

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : ((s : ↥I) → E ↑s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X (↑x) ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X (↑x) ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (X ↑s) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁸ : (s : S) → TopologicalSpace (E s)
inst✝⁷ : (s : S) → MeasurableSpace (E s)
inst✝⁶ : ∀ (s : S), BorelSpace (E s)
inst✝⁵ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝ : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : ((s : ↥I) → E ↑s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X (↑x) ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X (↑x) ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
I : Finset S
⊢ AEMeasurable U P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁴ : (s : S) → TopologicalSpace (E s)
inst✝³ : (s : S) → MeasurableSpace (E s)
inst✝² : ∀ (s : S), BorelSpace (E s)
inst✝¹ : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (I : Finset S) (f : (s : ↥I) → E ↑s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X (↑s) ω) ∂P
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (X ↑s) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁴ : (s : S) → TopologicalSpace (E s)
inst✝³ : (s : S) → MeasurableSpace (E s)
inst✝² : ∀ (s : S), BorelSpace (E s)
inst✝¹ : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (I : Finset S) (f : ((s : ↥I) → E ↑s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, f fun x ↦ X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X (↑x) ω ∂P
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (X ↑s) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))

Tactic:
by

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (binomial x h b) (Fin.ofNat (b + 1) k)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ log (rexp (↑c * t ^ 2 / 2)) ≤ ↑c * t ^ 2 / 2

Tactic:
by

Goal state after: