Documentation

Lean 4 Proof

theorem unnormCES_symmetricPoint {J : ℕ} (_hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    unnormCES J ρ (symmetricPoint J c) = (↑J : ℝ) ^ (1 / ρ) * c := by
  simp only [unnormCES, symmetricPoint]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  rw [mul_rpow (Nat.cast_nonneg J) (rpow_nonneg hc.le ρ)]
  congr 1
  rw [← rpow_mul hc.le, mul_one_div_cancel hρ, rpow_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:157

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file