Documentation

Lean 4 Proof

def PseudoAdditive (_S : (J : ℕ) → ℝ → (Fin J → ℝ) → ℝ) (_q : ℝ) : Prop :=
  ∀ (J₁ J₂ : ℕ) (_p₁ : Fin J₁ → ℝ) (_p₂ : Fin J₂ → ℝ),
    -- For independent product distributions p₁ ⊗ p₂:
    -- S(p₁ ⊗ p₂) = S(p₁) + S(p₂) + (1-q)·S(p₁)·S(p₂)
    True  -- statement formalized at the level of the property

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:36

Module Section

Theorem 2: Tsallis Uniqueness (Paper 2, Section 3.1)

In the same file