mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

Tactic:
refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
    · exact h_subset (add_half_inf_sub_mem_Ioo hlu)
    · exact h_subset (sub_half_inf_sub_mem_Ioo hlu)
    · positivity
    · exact lt_of_lt_of_le (by simp [ht]) (le_abs_self _)

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ ((covarianceBilinDual μ) ((toDualMap ℝ E) x)) ((toDualMap ℝ E) y) = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]

Tactic:
covarianceBilinDual_eq_covariance h

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ cov[⇑((toDualMap ℝ E) x), ⇑((toDualMap ℝ E) y); μ] = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (z : F),
      ⟪u, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ * ⟪v, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ ∂Measure.map (⇑L) μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), id x ∂μ⟫ ∂μ

pp: case h
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp id 2 (Measure.map (⇑L) μ)

Tactic:
· simp_rw [id, L.integral_id_map (h.integrable (by simp))]
    rw [integral_map]
    · simp_rw [← map_sub, ← L.adjoint_inner_left]
    all_goals fun_prop

Goal state after:
case h
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp id 2 (Measure.map (⇑L) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ charFun μ t = cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
rw [charFun_eq_charFunDual_toDualMap, IsGaussian.charFunDual_eq]

Goal state after:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ cexp ((∫ (x : E), ↑(((toDualMap ℝ E) t) x) ∂μ) * I - ↑Var[⇑((toDualMap ℝ E) t); μ] / 2) =
    cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ n, x ≤ t n

Tactic:
simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto

Goal state after:
β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
x : β
hx : t 0 < x
ht_tendsto : ∀ (b : β), ∃ a, b ≤ t a
⊢ ∃ n, x ≤ t n
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y

Tactic:
simp_rw [inner_smul_right, ← continuousLinearMapOfBilin_apply, ← covarianceOperator_inner hμ]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪(covarianceOperator μ) x, y⟫ =
    ⟪(continuousLinearMapOfBilin
          ((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
            (toDualMap ℝ E).toContinuousLinearMap))
        x,
      y⟫
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c + x) μ)

Tactic:
by simp_rw [add_comm c]; infer_instance

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
⊢ charFunDual (Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ)) = charFunDual (μ.prod μ)

Tactic:
ext L

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ charFunDual (Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ)) L = charFunDual (μ.prod μ) L
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : CompleteSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : NormedSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilinDual μ = covarianceBilinDual ν
⊢ charFunDual μ = charFunDual ν

Tactic:
ext L

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : CompleteSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : NormedSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilinDual μ = covarianceBilinDual ν
L : StrongDual ℝ E
⊢ charFunDual μ L = charFunDual ν L
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
⊢ charFunDual (Measure.map (⇑f) (stdGaussian E)) = charFunDual (stdGaussian F)

Tactic:
ext L

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
L : StrongDual ℝ F
⊢ charFunDual (Measure.map (⇑f) (stdGaussian E)) L = charFunDual (stdGaussian F) L
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
⊢ charFunDual μ = charFunDual (Measure.dirac (∫ (x : E), x ∂μ))

Tactic:
ext L

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = charFunDual (Measure.dirac (∫ (x : E), x ∂μ)) L
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * ↑s = ↑t - ↑s

Tactic:
two_mul,

Goal state after:
I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s + ↑t - (↑s + ↑s) = ↑t - ↑s
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t

Tactic:
two_mul,

Goal state after:
case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ min ↑s ↑t + min ↑s ↑t ≤ ↑s + ↑t
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFunDual (Measure.map (X + Y) P) = charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)

Tactic:
ext L

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (X + Y) P) L = (charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)) L
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
⊢ charFun (Measure.map (fun ω ↦ ∑ i ∈ s, X i ω) P) = ∏ i ∈ s, charFun (Measure.map (X i) P)

Tactic:
by
  convert! hX.charFun_map_finsetSum_eq_prod mX
  simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : 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 ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (Measure.map (fun ω ↦ toLp p fun x ↦ X x ω) P) L =
        ∏ i,
          charFunDual (Measure.map (X i) P)
            (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

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

Goal state before:
pp: case h₁
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} ≤ 1

Tactic:
exact prob_le_one

Goal state after:
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
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
⊢ MeasurableSet ((fun x ↦ ‖x‖ ≤ b) ⁻¹' {True})

Tactic:
show (fun x : E ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x : E | ‖x‖ ≤ b} by ext; simp

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
⊢ MeasurableSet {x | ‖x‖ ≤ b}
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable fun a ↦ ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ s ∈ range Iic, Measurable fun a ↦ (f a).measure s

Tactic:
simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]
    exact fun _ ↦ (hf _).ennreal_ofReal

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ AEMeasurable.mk (X i j) ⋯ ω) κ P

Tactic:
refine iIndepFun_process (fun i j ↦ (hX i j).measurable_mk) fun I J ↦ ?_

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
I : Finset S
J : (i : ↥I) → Finset (T ↑i)
⊢ iIndepFun (fun i ω j ↦ AEMeasurable.mk (X ↑i ↑j) ⋯ ω) κ P
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ stieltjesFunctionAux f a r

Tactic:
IsMeasurableRatCDF.stieltjesFunctionAux_def

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ ⨅ q, f a ↑q
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y

Tactic:
IsMeasurableRatCDF.stieltjesFunctionAux_def

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
⊢ ⨅ q, f a ↑q ≤ ⨅ q, f a ↑q
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
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
by_cases hρ_zero : (ν a).restrict s = 0

Goal state after:
case pos
α : 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 = (κ a) (s ×ˢ Iic x)

case neg
α : 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 = (κ a) (s ×ˢ Iic x)
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
q : ℚ
hq : x < ↑q
this : (κ a) (s ×ˢ Iic ↑q) = 0
⊢ (κ a) (s ×ˢ Iic x) = 0

Tactic:
refine measure_mono_null (fun p ↦ ?_) this

Goal state after:
α : 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
q : ℚ
hq : x < ↑q
this : (κ a) (s ×ˢ Iic ↑q) = 0
p : β × ℝ
⊢ p ∈ s ×ˢ Iic x → p ∈ s ×ˢ Iic ↑q
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ ∃ m f,
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (Measure.map (fun ω x ↦ X x ω) P) L = cexp (↑(L m) * I - ↑((f L) L) / 2)

Tactic:
refine ⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
⊢ charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
    cexp
      (↑(L fun i ↦ ∫ (x : E i), x ∂Measure.map (X i) P) * I -
        ↑(((diagonalStrongDualPi fun i ↦ covarianceBilinDual (Measure.map (X i) P)) L) L) / 2)
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 n ↦ f (a, t) (-↑n)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)

Tactic:
filter_upwards [this, hf.mono a] with t ht h_mono
    have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg
    exact (tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht

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

Goal state before:
pp: case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0) (t : ↑(Set.Iic t₀)), cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑t; P] = 0

Tactic:
rintro s ⟨t, ht : t ≤ t₀⟩

Goal state after:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
⊢ cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑⟨t, ht⟩; P] = 0
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
⊢ (fun ω t ↦ B (t₀ + t) ω - B t₀ ω) ⟂ᵢ[P] fun ω t ↦ B (↑t) ω

Tactic:
by
  have mX t := hB.aemeasurable t
  apply IsGaussianProcess.indepFun_of_covariance_eq_zero
  · apply hB.isGaussianProcess.of_isGaussianProcess
    rintro (t | ⟨t, ht⟩)
    · exact ⟨{t₀, t₀ + t},
        { toFun x := x ⟨t₀ + t, by simp⟩ - x ⟨t₀, by simp⟩
          map_add' x y := by simp; abel
          map_smul' c x := by simp; ring }, by simp⟩
    · exact ⟨{t},
        { toFun x := x ⟨t, by simp⟩
          map_add' x y := by simp
          map_smul' c x := by simp }, by simp⟩
  any_goals fun_prop
  · rintro s ⟨t, ht : t ≤ t₀⟩
    have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_fun_sub_left, hB.covariance_eval, hB.covariance_eval, min_eq_right, min_eq_right,
      sub_self]
    · grind
    · simp [ht, le_add_right]
    all_goals exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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 t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ (κ a) univ < ∞

Tactic:
exact measure_lt_top _ univ

Goal state after: