mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ ((EuclideanSpace.basisFun ι ℝ) i).ofLp ⬝ᵥ S *ᵥ ((EuclideanSpace.basisFun ι ℝ) j).ofLp = S i j

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)

Tactic:
·

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ ((EuclideanSpace.basisFun ι ℝ) i).ofLp ⬝ᵥ S *ᵥ ((EuclideanSpace.basisFun ι ℝ) j).ofLp = S i j
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)

Tactic:
·

Goal state after:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal ((EuclideanSpace.proj i) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[⇑(EuclideanSpace.proj i); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
·

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal ((EuclideanSpace.proj i) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[⇑(EuclideanSpace.proj i); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : μ {x | ‖x‖ ≤ a} = 1
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

pp: case neg
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

Tactic:
·

Goal state after:
case pos
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : μ {x | ‖x‖ ≤ a} = 1
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ ∫ (x : EuclideanSpace ℝ ↥J), id x ∂Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S) =
    ∫ (x : EuclideanSpace ℝ ↥J),
      id x ∂multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)

pp: case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ covarianceBilin (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)) =
    covarianceBilin
      (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩))

Tactic:
·

Goal state after:
case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ ∫ (x : EuclideanSpace ℝ ↥J), id x ∂Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S) =
    ∫ (x : EuclideanSpace ℝ ↥J),
      id x ∂multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I)
      (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

pp: case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
·

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I)
      (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e_μ
I : Finset ℝ≥0
s t : ↥I
⊢ ∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I = 0

pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal = nndist ↑s ↑t

Tactic:
·

Goal state after:
case e_μ
I : Finset ℝ≥0
s t : ↥I
⊢ ∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I = 0
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᵐ[μ] closedBall 0 a

pp: 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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Measurable fun x ↦ ‖x‖ ≤ a

Tactic:
·

Goal state after:
case pos
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᵐ[μ] closedBall 0 a
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

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

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

Tactic:
·

Goal state after:
case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e_v.inr
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t

pp: I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t

Tactic:
·

Goal state after:
case e_v.inr
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = ↑t + ↑s - 2 * min ↑t ↑s

pp: case e'_3
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ nndist ↑s ↑t = nndist ↑t ↑s

Tactic:
·

Goal state after:
case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = ↑t + ↑s - 2 * min ↑t ↑s
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

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

pp: case hv.hX
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

pp: case hv.hY
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

pp: case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)

pp: case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

Tactic:
·

Goal state after:
case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ cov[(fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI),
      (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI);
      multivariateGaussian μ S] =
    ((covarianceBilin
          (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)))
        ((EuclideanSpace.basisFun ↥J ℝ).toBasis i))
      ((EuclideanSpace.basisFun ↥J ℝ).toBasis j)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e'_3
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ nndist ↑s ↑t = nndist ↑t ↑s

Tactic:
·

Goal state after:
case e'_3
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ nndist ↑s ↑t = nndist ↑t ↑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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (Measure.map X P)

pp: case hg
Ω : 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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEStronglyMeasurable id (Measure.map X P)

pp: case hf
Ω : 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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEMeasurable X P

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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MeasurableSpace E

Tactic:
·

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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (Measure.map X P)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
·

Goal state after:
case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
·

Goal state after:
case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
·

Goal state after:
case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Measurable fun x ↦ ‖x‖ ≤ a

Tactic:
·

Goal state after:
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Measurable fun x ↦ ‖x‖ ≤ a
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
·

Goal state after:
case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
·

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ projectiveFamily J =
    Measure.map (Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I))

pp: case hg
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable (Finset.restrict₂ hJI)

pp: case hf
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
·

Goal state after:
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ projectiveFamily J =
    Measure.map (Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hg
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable (Finset.restrict₂ hJI)

pp: case hf
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
·

Goal state after:
case hg
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable (Finset.restrict₂ hJI)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hf
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
·

Goal state after:
case hf
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)

pp: case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

Tactic:
·

Goal state after:
case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

Tactic:
·

Goal state after:
case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))