Documentation

Lean 4 Proof

theorem network_log_premium (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    Real.log (unnormCES J ρ (symmetricPoint J c) / c) =
      1 / ρ * Real.log ↑J := by
  rw [unnormCES_symmetricPoint hJ hρ hc]
  rw [mul_div_cancel_right₀ _ (ne_of_gt hc)]
  exact Real.log_rpow (by exact_mod_cast hJ : (0 : ℝ) < ↑J) (1 / ρ)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:838

Module Section

## Network Scaling Results

In the same file