Nonnegative Value of Free Information

Abstract

A free ignorable observation cannot lower optimal expected value.

Theorem 1.1 (Free ignorable information has nonnegative value).

$$\begin{array}{r}\forall X,E,U:\mathrm{Type},\\ \forall \mathbb{E}:\mathrm{Concept}\left(X\to \mathbb{R},\mathbb{R}\right),\\ \forall observe:\mathrm{Concept}\left(X,E\right),worldAfterObservation:E\to X\to X,\\ \forall V:\mathrm{Concept}\left(X,U\to \mathbb{R}\right),informationCost:\mathbb{R},\\ \forall A0:\mathrm{Set}\left(U\right),A1:E\to \mathrm{Set}\left(U\right),\\ \forall P:\mathrm{Set}\left(E\to U\right),W_0,W_E:\mathbb{R},\\ \forall informationFree:informationCost=0,\\ \forall observationDoesNotChangeWorld:\forall e:E,x:X,worldAfterObservation(e,x)=x,\\ \forall canIgnoreInformation:\forall u:U,u\in A0\Rightarrow (e:E)\mapsto u\in P,\\ \forall actionSetNotReduced:\forall e:E,A0\subseteq A1(e),\\ \forall uninformedOptimal:\mathrm{IsGreatest}\left(\mathrm{image}\left(\mathrm{uninformedExpectedValue}\left(\mathbb{E},V\right),A0\right),W_0\right),\\ \forall informedOptimal:\mathrm{IsGreatest}\left(\mathrm{image}\left(\mathrm{informedExpectedValue}\left(\mathbb{E},observe,worldAfterObservation,V,informationCost\right),\mathrm{admissiblePolicies}\left(P,A1\right)\right),W_E\right),\\ W_0\le W_E.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValue/FreeInformationValue.free_ignorable_information_value_nonnegative (✓ std3). ∎

Source. Repository-derived.

Commentary.

The uninformed value is the greatest expected utility obtained by choosing one available action. The informed value is the greatest net expected utility of an admissible observation-dependent policy.

The four safeguards are public. Information has zero cost, observation leaves the state unchanged, every constant policy is a permitted way to ignore the observation, and every previously available action remains available after each observation.

Choose an action attaining the uninformed optimum. Its constant policy is both permitted and pointwise available by the last two safeguards. The first two safeguards make its informed net value equal to the uninformed optimum, so informed optimality gives the inequality.

The expectation functional, observation, world transition, utility, costs, action sets, and policy set are independent source inputs. Repository and pinned-library searches found no exact theorem combining them.

References

• Truth anchor: D5/S3/ConceptDynamics/DecisionValue/FreeInformationValue.free_ignorable_information_value_nonnegative
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition