internlm/Lean-Github huggingface dataset:
Theorem: TrussDesign.σₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 0.5
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.F₁ₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < F₁ₚ
Tactic:
unfold F₁ₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 10
Theorem: TrussDesign.F₁ₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.F₂ₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < F₂ₚ
Tactic:
unfold F₂ₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 20
Theorem: TrussDesign.F₂ₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 20
Tactic:
norm_num
Proof state after:
no goals
Theorem: gaussianPdf_pos
Proof state before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < gaussianPdf R y
Tactic:
refine' mul_pos (div_pos zero_lt_one (sqrt_pos.2 (mul_pos _ h.det_pos))) (exp_pos _)
Proof state after:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < (2 * π) ^ n
Theorem: gaussianPdf_pos
Proof state before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < (2 * π) ^ n
Tactic:
exact (pow_pos (mul_pos (by positivity) pi_pos) n)
Proof state after:
no goals
Theorem: gaussianPdf_pos
Proof state before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < 2
Tactic:
positivity
Proof state after:
no goals
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
have : ∀ i,
  i ∈ Finset.univ → gaussianPdf R (y i) ≠ 0 := fun i _ => ne_of_gt (gaussianPdf_pos _ _ hR)
Proof state after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
have sqrt_2_pi_n_R_det_ne_zero: sqrt ((2 * π) ^ n * R.det) ≠ 0 := by
  refine' ne_of_gt (sqrt_pos.2 (mul_pos _ hR.det_pos))
  exact (pow_pos (mul_pos (by positivity) pi_pos) _)
Proof state after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
rw [log_prod Finset.univ (fun i => gaussianPdf R (y i)) this]
Proof state after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
unfold gaussianPdf
Proof state after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
apply congr_arg (Finset.sum Finset.univ)
Proof state after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (fun i => (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log) = fun i =>
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (fun i => (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log) = fun i =>
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2
Tactic:
ext i
Proof state after:
case h
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2
Theorem: log_prod_gaussianPdf
Proof state before:
case h
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2
Tactic:
rw [log_mul, log_div, sqrt_mul, log_mul, log_exp, log_one, zero_sub]
Proof state after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ¬((2 * π) ^ n).sqrt = 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact ne_of_gt (sqrt_pos.2 (pow_pos (mul_pos (by positivity) pi_pos) _))
Proof state after:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact ne_of_gt (sqrt_pos.2 hR.det_pos)
Proof state after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact pow_nonneg (mul_nonneg (by positivity) (le_of_lt pi_pos)) _
Proof state after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
norm_num
Proof state after:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact sqrt_2_pi_n_R_det_ne_zero
Proof state after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact div_ne_zero (by norm_num) sqrt_2_pi_n_R_det_ne_zero
Proof state after:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Theorem: log_prod_gaussianPdf
Proof state before:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact exp_ne_zero _
Proof state after:
no goals
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0
Tactic:
refine' ne_of_gt (sqrt_pos.2 (mul_pos _ hR.det_pos))
Proof state after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ 0 < (2 * π) ^ n
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ 0 < (2 * π) ^ n
Tactic:
exact (pow_pos (mul_pos (by positivity) pi_pos) _)
Proof state after:
no goals
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ 0 < 2
Tactic:
positivity
Proof state after:
no goals
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 < 2
Tactic:
positivity
Proof state after:
no goals
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: log_prod_gaussianPdf
Proof state before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: sum_quadForm
Proof state before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Tactic:
by_cases h : m = 0
Proof state after:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace

case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Theorem: sum_quadForm
Proof state before:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace

case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Tactic:
{ subst h; simp }
Proof state after:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace