mathlib-initiative/mathlib-tactics huggingface dataset:
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:
fun_prop

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:
fun_prop

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:
fun_prop

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:
fun_prop

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:
fun_prop

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:
fun_prop

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:
fun_prop

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 : Integrable (fun y ↦ rexp (0 * X y)) (κ ω')
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → IsFiniteMeasure (κ ω')

Tactic:
h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : Integrable (fun y ↦ rexp (0 * X y)) (κ ω')
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ IsFiniteMeasure (κ ω')
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ AEStronglyMeasurable (fun ω ↦ edist (X s ω) (X t ω)) P

Tactic:
refine ⟨(fun ω ↦ edist (hX.mk X s ω) (hX.mk X t ω)),
    hX.IsKolmogorovProcess_mk.stronglyMeasurable_edist, ?_⟩
  filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂ using by simp [hω₁, hω₂]

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 : IsFiniteMeasure (κ ω')
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → (κ ω') Set.univ ≤ 1

Tactic:
h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure (κ ω')
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ (κ ω') Set.univ ≤ 1
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' f μ
hf : ∀ (i : ι), Measurable (f i)
i✝ j✝ k l : ι
hik : i✝ ≠ k
hil : i✝ ≠ l
hjk : j✝ ≠ k
hjl : j✝ ≠ l
g : (i j : ι) → ((x : ↥{i, j}) → β ↑x) → β i × β j := fun i j v ↦ (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
i j : ι
⊢ Measurable (g i j)

Tactic:
fun_prop

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 : IsFiniteMeasure (κ ω')
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
this : (κ ω').real Set.univ ≤ 1
⊢ (κ ω') Set.univ ≤ ENNReal.ofReal 1

Tactic:
ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) zero_le_one

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure (κ ω')
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
this : (κ ω').real Set.univ ≤ 1
⊢ ((κ ω') Set.univ).toReal ≤ 1
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝⁴ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
⊢ Measurable fun ω ↦ (X s ω, X t ω)

Tactic:
fun_prop

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_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ (q : ℚ), ∀ᵐ (ω' : Ω') ∂ν, mgf X (κ ω') ↑q ≤ rexp (↑c * ↑q ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
rw [← ae_all_iff] at h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
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_int✝ : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
ω' : Ω'
⊢ (∀ (i : ℚ), mgf X (κ ω') ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)) →
    (∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')) → ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int✝ : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf✝ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
ω' : Ω'
h_mgf : ∀ (i : ℚ), mgf X (κ ω') ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
⊢ (∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')) → ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
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_int✝¹ : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf✝ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int✝ : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
ω' : Ω'
h_mgf : ∀ (i : ℚ), mgf X (κ ω') ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ Continuous fun b ↦ rexp (↑c * b ^ 2 / 2)

Tactic:
fun_prop

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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) →
    (∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω) → ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ (∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω) → ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
t : ℝ
h1 : Integrable (fun ω ↦ rexp (t * X ω)) (Measure.map Y (⇑κ ∘ₘ ν))
⊢ AEMeasurable Y (⇑κ ∘ₘ ν)

Tactic:
fun_prop

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

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

Tactic:
h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
ω' : Ω'
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) ((κ.map Y) ω')
h_mgf : ∀ (t : ℝ), mgf X ((κ.map Y) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), mgf (X ∘ Y) (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

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

Tactic:
fun_prop

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 : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ Measurable 0

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 : ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ), ∀ (t : ℝ), mgf Y (η ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ AEMeasurable Prod.snd (ν ⊗ₘ κ)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ Continuous fun x ↦ 2 / (↑k + 1) * x ^ 2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ Continuous (HMul.hMul 2)

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
⊢ (∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)) →
    μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω' →
      μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
h_mgf

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
h_mgf : ∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω' →
    μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF X c (Measure.map Y μ)
t : ℝ
h1 : Integrable (fun ω ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ AEMeasurable Y μ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Measurable fun ω ↦ rexp (t * X ω)

Tactic:
fun_prop

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

Goal state before:
pp: case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf Y μ t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
exact hY.mgf_le t

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : HasSubgaussianMGF (fun ω ↦ ∑ i, X (↑i) ω) (∑ i ∈ s, c i) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
exact this.congr (ae_of_all _ fun ω ↦ Finset.sum_attach s (fun i ↦ X i ω))

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ Measurable fun x ↦ x - ∫ (x : Ω), Y x ∂μ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ Measurable fun x ↦ x - ∫ (x : Ω), X x ∂μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ ↑e.symm ∘ₗ σ g = ρ g ∘ₗ ↑e.symm

Tactic:
by
  apply e.comp_toLinearMap_eq_iff _ _ |>.1
  rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
⊢ ∃ k, ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ

Tactic:
simp_rw [Pi.sub_apply, norm_sub_rev (X 0 _)]
    exact ((tendsto_order.1 (tendsto_integral_norm_approxOn_sub h'.measurable hint)).2 δ
      δpos).exists

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hω : Tendsto (fun e ↦ ‖(↑e)⁻¹ • ∑ i ∈ Finset.range e, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖) atTop (𝓝 0)
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
⊢ ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ

Tactic:
exact (tendsto_order.1 hω).2 δ δpos

Goal state after: