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

Goal state before:
pp: case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ⋯
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ≤ 2 * ‖y‖

Tactic:
;

Goal state after:
case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ⋯
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ≤ 2 * ‖y‖
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ⋯
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ 0 ≤ 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
;

Goal state after:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ⋯
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ 0 ≤ 2 ^ ↑p * ‖y - c‖ ^ ↑p
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
L : StrongDual ℝ E
x : Fin (finrank ℝ E) → ℝ
⊢ (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) x = (∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i) x

Tactic:
;

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
x : Fin (finrank ℝ E) → ℝ
⊢ (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) x = (∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i) x
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hx.refine_2
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - c).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]
      exact ⟨h.trans_lt hd, by finiteness⟩

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

Goal state before:

Tactic:
C' * ‖x‖ ^ 2
  _ ≤ C' * ((1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2) := by gcongr
  _ = C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2 := by grind

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i✝ j i : ι
x✝ : EuclideanSpace ℝ ι
⊢ x✝.ofLp i = ⟪(EuclideanSpace.basisFun ι ℝ) i, x✝⟫

Tactic:
;

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i✝ j i : ι
x✝ : EuclideanSpace ℝ ι
⊢ x✝.ofLp i = ⟪(EuclideanSpace.basisFun ι ℝ) i, x✝⟫
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
i✝ j✝ : ↥I
⊢ covMatrix I i✝ j✝ = Matrix.of (fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)) i✝ j✝

Tactic:
;

Goal state after:
I : Finset ℝ≥0
i✝ j✝ : ↥I
⊢ covMatrix I i✝ j✝ = Matrix.of (fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)) i✝ j✝
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
| fun x ↦ x s

Tactic:
;

Goal state after:
I : Finset ℝ≥0
s : ↥I
| fun x ↦ x s
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
⊢ HasGaussianLaw X P

Tactic:
refine ⟨isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ charFunDual (Measure.map X P) t = cexp ((∫ (x : E), ↑(t x) ∂Measure.map X P) * I - ↑Var[⇑t; Measure.map X P] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i✝ j i : ↥J
x✝ : EuclideanSpace ℝ ↥I
⊢ ((fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI)) x✝ = x✝.ofLp ⟨↑i, ⋯⟩

Tactic:
;

Goal state after:
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i✝ j i : ↥J
x✝ : EuclideanSpace ℝ ↥I
⊢ ((fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI)) x✝ = x✝.ofLp ⟨↑i, ⋯⟩
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
x✝ : Ω
⊢ (∑ i, X i) x✝ = (⇑(∑ i, ContinuousLinearMap.proj i) ∘ fun ω x ↦ X x ω) x✝

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
x✝ : Ω
⊢ (∑ i, X i) x✝ = (⇑(∑ i, ContinuousLinearMap.proj i) ∘ fun ω x ↦ X x ω) x✝
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I J : Finset ℝ≥0
hJI : J ⊆ I
x✝¹ : WithLp 2 (↥I → ℝ)
x✝ : ↥J
⊢ (Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) x✝¹ x✝ =
    (ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)) x✝¹ x✝

Tactic:
;

Goal state after:
I J : Finset ℝ≥0
hJI : J ⊆ I
x✝¹ : WithLp 2 (↥I → ℝ)
x✝ : ↥J
⊢ (Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) x✝¹ x✝ =
    (ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)) x✝¹ x✝
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case empty
Ω : 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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
mX : ∀ i ∈ ∅, AEMeasurable (X i) P
hX : iIndepFun (∅.restrict X) P
x✝ : StrongDual ℝ E
⊢ charFunDual (Measure.map (∑ i ∈ ∅, X i) P) x✝ = (∏ i ∈ ∅, charFunDual (Measure.map (X i) P)) x✝

Tactic:
;

Goal state after:
case empty
Ω : 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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
mX : ∀ i ∈ ∅, AEMeasurable (X i) P
hX : iIndepFun (∅.restrict X) P
x✝ : StrongDual ℝ E
⊢ charFunDual (Measure.map (∑ i ∈ ∅, X i) P) x✝ = (∏ i ∈ ∅, charFunDual (Measure.map (X i) P)) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x✝ : Fin n
⊢ (x + y) ⟨t x✝.succ, ⋯⟩ - (x + y) ⟨t x✝.castSucc, ⋯⟩ =
    ((fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) + fun i ↦ y ⟨t i.succ, ⋯⟩ - y ⟨t i.castSucc, ⋯⟩) x✝

Tactic:
;

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x✝ : Fin n
⊢ (x + y) ⟨t x✝.succ, ⋯⟩ - (x + y) ⟨t x✝.castSucc, ⋯⟩ =
    ((fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) + fun i ↦ y ⟨t i.succ, ⋯⟩ - y ⟨t i.castSucc, ⋯⟩) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x✝ : Fin n
⊢ x ⟨t x✝.succ, ⋯⟩ + y ⟨t x✝.succ, ⋯⟩ - (x ⟨t x✝.castSucc, ⋯⟩ + y ⟨t x✝.castSucc, ⋯⟩) =
    x ⟨t x✝.succ, ⋯⟩ - x ⟨t x✝.castSucc, ⋯⟩ + (y ⟨t x✝.succ, ⋯⟩ - y ⟨t x✝.castSucc, ⋯⟩)

Tactic:
;

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x✝ : Fin n
⊢ x ⟨t x✝.succ, ⋯⟩ + y ⟨t x✝.succ, ⋯⟩ - (x ⟨t x✝.castSucc, ⋯⟩ + y ⟨t x✝.castSucc, ⋯⟩) =
    x ⟨t x✝.succ, ⋯⟩ - x ⟨t x✝.castSucc, ⋯⟩ + (y ⟨t x✝.succ, ⋯⟩ - y ⟨t x✝.castSucc, ⋯⟩)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x✝ : Fin n
⊢ (m • x) ⟨t x✝.succ, ⋯⟩ - (m • x) ⟨t x✝.castSucc, ⋯⟩ =
    ((RingHom.id ℝ) m • fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) x✝

Tactic:
;

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x✝ : Fin n
⊢ (m • x) ⟨t x✝.succ, ⋯⟩ - (m • x) ⟨t x✝.castSucc, ⋯⟩ =
    ((RingHom.id ℝ) m • fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x✝ : Fin n
⊢ m • x ⟨t x✝.succ, ⋯⟩ - m • x ⟨t x✝.castSucc, ⋯⟩ = m • (x ⟨t x✝.succ, ⋯⟩ - x ⟨t x✝.castSucc, ⋯⟩)

Tactic:
;

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x✝ : Fin n
⊢ m • x ⟨t x✝.succ, ⋯⟩ - m • x ⟨t x✝.castSucc, ⋯⟩ = m • (x ⟨t x✝.succ, ⋯⟩ - x ⟨t x✝.castSucc, ⋯⟩)
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case convert_9
Ω : 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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
e : ↥(insert i s) → ι := Subtype.val
x✝ : ↥(insert i s)
a✝ : x✝ ∈ ↑{x | ↑x ∈ s}
⊢ ↑x✝ ∈ ↑s

Tactic:
;

Goal state after:
case convert_9
Ω : 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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
e : ↥(insert i s) → ι := Subtype.val
x✝ : ↥(insert i s)
a✝ : x✝ ∈ ↑{x | ↑x ∈ s}
⊢ ↑x✝ ∈ ↑s
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case convert_10
Ω : 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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
e : ↥(insert i s) → ι := Subtype.val
⊢ ∀ i_1 ∈ s, (i_1 = i ∨ i_1 ∈ s → i_1 ∈ s → ¬i_1 = i ∧ i_1 ∉ s) → X i_1 = 0

Tactic:
;

Goal state after:
case convert_10
Ω : 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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
e : ↥(insert i s) → ι := Subtype.val
⊢ ∀ i_1 ∈ s, (i_1 = i ∨ i_1 ∈ s → i_1 ∈ s → ¬i_1 = i ∧ i_1 ∉ s) → X i_1 = 0
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
x y : ↥(I.biUnion J) → E
x✝ : ↥I
⊢ ((L ↑x✝) fun t ↦ (x + y) ⟨↑t, ⋯⟩) = ((fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) + fun s ↦ (L ↑s) fun t ↦ y ⟨↑t, ⋯⟩) x✝

Tactic:
;

Goal state after:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
x y : ↥(I.biUnion J) → E
x✝ : ↥I
⊢ ((L ↑x✝) fun t ↦ (x + y) ⟨↑t, ⋯⟩) = ((fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) + fun s ↦ (L ↑s) fun t ↦ y ⟨↑t, ⋯⟩) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
c : ℝ
x : ↥(I.biUnion J) → E
x✝ : ↥I
⊢ ((L ↑x✝) fun t ↦ (c • x) ⟨↑t, ⋯⟩) = ((RingHom.id ℝ) c • fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) x✝

Tactic:
;

Goal state after:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
c : ℝ
x : ↥(I.biUnion J) → E
x✝ : ↥I
⊢ ((L ↑x✝) fun t ↦ (c • x) ⟨↑t, ⋯⟩) = ((RingHom.id ℝ) c • fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) x✝
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 (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFun (Measure.map (X i) P)

Tactic:
ext
  simp [charFun_eq_charFunDual_toDualMap, hX.charFunDual_map_finsetSum_eq_prod mX]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  { toFun := fun x s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
x✝¹ : Ω
x✝ : ↥I
⊢ I.restrict (fun x ↦ Y x x✝¹) x✝ = (⇑K ∘ fun ω ↦ (I.biUnion J).restrict fun x ↦ X x ω) x✝¹ x✝

Tactic:
;

Goal state after:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  { toFun := fun x s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
x✝¹ : Ω
x✝ : ↥I
⊢ I.restrict (fun x ↦ Y x x✝¹) x✝ = (⇑K ∘ fun ω ↦ (I.biUnion J).restrict fun x ↦ X x ω) x✝¹ x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
x y : ↥{t₀, t₀ + t} → E
⊢ x ⟨t₀ + t, ⋯⟩ + y ⟨t₀ + t, ⋯⟩ - (x ⟨t₀, ⋯⟩ + y ⟨t₀, ⋯⟩) = x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩ + (y ⟨t₀ + t, ⋯⟩ - y ⟨t₀, ⋯⟩)

Tactic:
;

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
x y : ↥{t₀, t₀ + t} → E
⊢ x ⟨t₀ + t, ⋯⟩ + y ⟨t₀ + t, ⋯⟩ - (x ⟨t₀, ⋯⟩ + y ⟨t₀, ⋯⟩) = x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩ + (y ⟨t₀ + t, ⋯⟩ - y ⟨t₀, ⋯⟩)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
c : ℝ
x : ↥{t₀, t₀ + t} → E
⊢ c • x ⟨t₀ + t, ⋯⟩ - c • x ⟨t₀, ⋯⟩ = c • (x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩)

Tactic:
;

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
c : ℝ
x : ↥{t₀, t₀ + t} → E
⊢ c • x ⟨t₀ + t, ⋯⟩ - c • x ⟨t₀, ⋯⟩ = c • (x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
x y : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
x✝¹ : ↥I
x✝ : ↥(J x✝¹)
⊢ (x + y) ⟨⟨↑x✝¹, ↑x✝⟩, ⋯⟩ = ((fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) + fun i j ↦ y ⟨⟨↑i, ↑j⟩, ⋯⟩) x✝¹ x✝

Tactic:
;

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
x y : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
x✝¹ : ↥I
x✝ : ↥(J x✝¹)
⊢ (x + y) ⟨⟨↑x✝¹, ↑x✝⟩, ⋯⟩ = ((fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) + fun i j ↦ y ⟨⟨↑i, ↑j⟩, ⋯⟩) x✝¹ x✝