Documentation

Lean 4 Proof

theorem detection_asymmetry [NeZero J] (hJ : 0 < J)
    {ρ : ℝ} (hρ : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    -- (a) Aggregate is ρ-invariant at symmetry
    powerMean J ρ hρ (symmetricPoint J c) = c ∧
    -- (b) Fisher information is zero (information shadow)
    fisherInfoRho (symmetricPoint J c) ρ = 0 ∧
    -- (c) Gradient is orthogonal to 1⊥ (F insensitive to informative perturbations)
    (∀ v : Fin J → ℝ, orthToOne J v →
      ∑ j : Fin J, (1 / (↑J : ℝ)) * v j = 0) ∧
    -- (d) All log-ratios vanish at symmetry (no contrast signal)
    (∀ j k : Fin J, logRatio (symmetricPoint J c) j k = 0) :=
  ⟨powerMean_symmetricPoint hJ hρ hc,
   fisherInfoRho_zero_at_symmetry hc ρ,
   fun v hv => gradient_orthogonal_to_onePerp v hv,
   fun j k => logRatio_zero_at_symmetry c j k⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:531

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file