Documentation

Lean 4 Proof

theorem dual_curvature_principle [NeZero J]
    (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) (hρ0 : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c)
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) :
    -- (i) K is positive (economic curvature exists)
    0 < curvatureK J ρ ∧
    -- (ii) The CES-partition identity holds: F^ρ = Z/J
    powerMean J ρ hρ0 x ^ ρ = (1 / ↑J) * escortPartitionZ x ρ ∧
    -- (iii) K decomposes via bridge × geometry × Fisher
    curvatureK J ρ =
      bridgeRatio ρ * (↑J - 1) * c ^ 2 *
        escortFisherEigenvalue J ρ c ∧
    -- (iv) At symmetry, Fisher info for ρ is zero (estimation paradox)
    escortVariance (fun _ : Fin J => c) ρ
      (fun _ => Real.log c) = 0 :=
  ⟨curvatureK_pos hJ hρ,
   ces_pow_eq_mean_partition hρ0 x hx,
   curvatureK_eq_bridge_times_fisher hρ0 hc.ne'
     (Nat.cast_ne_zero.mpr (by omega)),
   escort_fisher_zero_at_symmetry hc ρ⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:1014

Module Section

### Part F: The Dual Curvature Principle

In the same file