Universal event spaces for an infinite Boolean algebra

This file supplies two complementary universal realizations of a Boolean algebra.

• PrimePoint B and stoneIndicator are the usual Stone representation by characteristic functions on prime ideals. This representation is faithful and is convenient for stating Scott's finite-sum cancellation condition.
• ProbabilityPoint B and eventVector evaluate an event at every finitely additive probability. Their real span is a normed order-unit space on which probabilities are exactly the point-evaluation positive normalized continuous linear functionals.

The second realization is used for the direct state correspondence below. Constructing the analogous functional on the Stone-indicator span requires the separate simple-function integration theorem for arbitrary finitely additive charges.

The probability-evaluation event space

def Scott1964.MeasurementStructures.Probability.Infinite.ProbabilityPoint (B : Type u) [BooleanAlgebra B] : Type u

A point of the universal probability-evaluation space.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.ProbabilityPoint B = { μ : B → ℝ // Scott1964.MeasurementStructures.IsFinitelyAdditiveProbability μ }

@[instance_reducible]

instance Scott1964.MeasurementStructures.Probability.Infinite.instTopologicalSpaceProbabilityPoint (B : Type u) [BooleanAlgebra B] : TopologicalSpace (ProbabilityPoint B)

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.instTopologicalSpaceProbabilityPoint B = ⊥

theorem Scott1964.MeasurementStructures.Probability.Infinite.probabilityPoint_discrete_eq_bot (B : Type u) [BooleanAlgebra B] : instTopologicalSpaceProbabilityPoint B = ⊥

instance Scott1964.MeasurementStructures.Probability.Infinite.instDiscreteTopologyProbabilityPoint (B : Type u) [BooleanAlgebra B] : DiscreteTopology (ProbabilityPoint B)

theorem Scott1964.MeasurementStructures.Probability.Infinite.probabilityPoint_nonnegative (B : Type u) [BooleanAlgebra B] (p : ProbabilityPoint B) (a : B) : 0 ≤ ↑p a

theorem Scott1964.MeasurementStructures.Probability.Infinite.probabilityPoint_le_one (B : Type u) [BooleanAlgebra B] (p : ProbabilityPoint B) (a : B) : ↑p a ≤ 1

theorem Scott1964.MeasurementStructures.Probability.Infinite.eventVector_dist_le_one (B : Type u) [BooleanAlgebra B] (a : B) (p q : ProbabilityPoint B) : dist (↑p a) (↑q a) ≤ 1

def Scott1964.MeasurementStructures.Probability.Infinite.eventVector (B : Type u) [BooleanAlgebra B] (a : B) : BoundedContinuousFunction (ProbabilityPoint B) ℝ

The universal evaluation vector μ ↦ μ(a) of an event.

Equations

• One or more equations did not get rendered due to their size.

def Scott1964.MeasurementStructures.Probability.Infinite.EventSpan (B : Type u) [BooleanAlgebra B] : Submodule ℝ (BoundedContinuousFunction (ProbabilityPoint B) ℝ)

The real normed space generated by universal event-evaluation vectors.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.EventSpan B = Submodule.span ℝ (Set.range (Scott1964.MeasurementStructures.Probability.Infinite.eventVector B))

def Scott1964.MeasurementStructures.Probability.Infinite.event (B : Type u) [BooleanAlgebra B] (a : B) : ↥(EventSpan B)

The event vector as an element of EventSpan.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.event B a = ⟨Scott1964.MeasurementStructures.Probability.Infinite.eventVector B a, ⋯⟩

Stone points and indicator vectors

structure Scott1964.MeasurementStructures.Probability.Infinite.PrimePoint (B : Type u) [BooleanAlgebra B] : Type u

A Stone point of B, presented as a prime (equivalently maximal) ideal.

• ideal : Order.Ideal B

  The ideal of events absent at this Stone point.

• isPrime : self.ideal.IsPrime

@[instance_reducible]

instance Scott1964.MeasurementStructures.Probability.Infinite.instTopologicalSpacePrimePoint (B : Type u) [BooleanAlgebra B] : TopologicalSpace (PrimePoint B)

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.instTopologicalSpacePrimePoint B = ⊥

instance Scott1964.MeasurementStructures.Probability.Infinite.instDiscreteTopologyPrimePoint (B : Type u) [BooleanAlgebra B] : DiscreteTopology (PrimePoint B)

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.stoneValue (B : Type u) [BooleanAlgebra B] (a : B) (p : PrimePoint B) : ℝ

The 0/1 value of an event at a Stone point.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.stoneValue B a p = if a ∈ p.ideal then 0 else 1

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator (B : Type u) [BooleanAlgebra B] (a : B) : BoundedContinuousFunction (PrimePoint B) ℝ

The characteristic vector of an event on the Stone points of B.

The convention is that a point lies in the event a exactly when its prime ideal does not contain a.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator B a = BoundedContinuousFunction.mkOfDiscrete (Scott1964.MeasurementStructures.Probability.Infinite.stoneValue B a) 1 ⋯

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator_apply (B : Type u) [BooleanAlgebra B] (a : B) (p : PrimePoint B) : (stoneIndicator B a) p = stoneValue B a p

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator_bot (B : Type u) [BooleanAlgebra B] : stoneIndicator B ⊥ = 0

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator_top (B : Type u) [BooleanAlgebra B] : stoneIndicator B ⊤ = 1

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator_sup_of_disjoint (B : Type u) [BooleanAlgebra B] {a b : B} (h : Disjoint a b) : stoneIndicator B (a ⊔ b) = stoneIndicator B a + stoneIndicator B b

theorem Scott1964.MeasurementStructures.Probability.Infinite.stoneIndicator_injective (B : Type u) [BooleanAlgebra B] : Function.Injective (stoneIndicator B)

Stone indicators separate events, so the Stone representation is faithful.

def Scott1964.MeasurementStructures.Probability.Infinite.IndicatorSumEqual (B : Type u) [BooleanAlgebra B] {ι : Type u_1} [Fintype ι] (x y : ι → B) : Prop

Equality of two finite sums of event indicators.

Equations

• One or more equations did not get rendered due to their size.

theorem Scott1964.MeasurementStructures.Probability.Infinite.indicatorSumEqual_iff (B : Type u) [BooleanAlgebra B] {ι : Type u_1} [Fintype ι] (x y : ι → B) : IndicatorSumEqual B x y ↔ ∀ (p : PrimePoint B), ∑ i : ι, stoneValue B (x i) p = ∑ i : ι, stoneValue B (y i) p

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.primeProbability (B : Type u) [BooleanAlgebra B] (p : PrimePoint B) : ProbabilityPoint B

The two-valued finitely additive probability associated with a Stone point.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.primeProbability B p = ⟨fun (a : B) => Scott1964.MeasurementStructures.Probability.Infinite.stoneValue B a p, ⋯⟩

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.primeProbability_apply (B : Type u) [BooleanAlgebra B] (p : PrimePoint B) (a : B) : ↑(primeProbability B p) a = stoneValue B a p

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.eventVector_apply (B : Type u) [BooleanAlgebra B] (a : B) (p : ProbabilityPoint B) : (eventVector B a) p = ↑p a

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.eventVector_bot (B : Type u) [BooleanAlgebra B] : eventVector B ⊥ = 0

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.eventVector_top (B : Type u) [BooleanAlgebra B] : eventVector B ⊤ = 1

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.eventVector_sup_of_disjoint (B : Type u) [BooleanAlgebra B] {a b : B} (h : Disjoint a b) : eventVector B (a ⊔ b) = eventVector B a + eventVector B b

theorem Scott1964.MeasurementStructures.Probability.Infinite.eventVector_injective (B : Type u) [BooleanAlgebra B] : Function.Injective (eventVector B)

Probability-evaluation vectors are also a faithful representation of events.

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.event_apply (B : Type u) [BooleanAlgebra B] (a : B) (p : ProbabilityPoint B) : ↑(event B a) p = ↑p a

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.event_bot (B : Type u) [BooleanAlgebra B] : event B ⊥ = 0

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.event_top_coe (B : Type u) [BooleanAlgebra B] : ↑(event B ⊤) = 1

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.event_sup_of_disjoint (B : Type u) [BooleanAlgebra B] {a b : B} (h : Disjoint a b) : event B (a ⊔ b) = event B a + event B b

def Scott1964.MeasurementStructures.Probability.Infinite.IsPositive (B : Type u) [BooleanAlgebra B] (L : ↥(EventSpan B) →L[ℝ] ℝ) : Prop

Pointwise positivity for a functional on the event span.

Equations

• One or more equations did not get rendered due to their size.

structure Scott1964.MeasurementStructures.Probability.Infinite.PositiveState (B : Type u) [BooleanAlgebra B] : Type u

A positive normalized bounded linear functional on the universal event span.

• functional : ↥(EventSpan B) →L[ℝ] ℝ

  The continuous linear evaluator whose values on events give the probability.

• positive : IsPositive B self.functional
• normalized : self.functional (event B ⊤) = 1

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.probabilityToState (B : Type u) [BooleanAlgebra B] (p : ProbabilityPoint B) : PositiveState B

Evaluation at a finitely additive probability is a positive normalized state.

Equations

• One or more equations did not get rendered due to their size.

theorem Scott1964.MeasurementStructures.Probability.Infinite.PositiveState.ext (B : Type u) [BooleanAlgebra B] {S T : PositiveState B} (h : S.functional = T.functional) : S = T

theorem Scott1964.MeasurementStructures.Probability.Infinite.PositiveState.ext_iff {B : Type u} [BooleanAlgebra B] {S T : PositiveState B} : S = T ↔ S.functional = T.functional

def Scott1964.MeasurementStructures.Probability.Infinite.stateToProbability (B : Type u) [BooleanAlgebra B] (S : PositiveState B) : ProbabilityPoint B

A positive normalized state restricts to a finitely additive probability on events.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.stateToProbability B S = ⟨fun (a : B) => S.functional (Scott1964.MeasurementStructures.Probability.Infinite.event B a), ⋯⟩

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.stateToProbability_apply (B : Type u) [BooleanAlgebra B] (S : PositiveState B) (a : B) : ↑(stateToProbability B S) a = S.functional (event B a)

@[simp]

theorem Scott1964.MeasurementStructures.Probability.Infinite.stateToProbability_probabilityToState (B : Type u) [BooleanAlgebra B] (p : ProbabilityPoint B) : stateToProbability B (probabilityToState B p) = p

theorem Scott1964.MeasurementStructures.Probability.Infinite.probabilityToState_stateToProbability (B : Type u) [BooleanAlgebra B] (S : PositiveState B) : probabilityToState B (stateToProbability B S) = S

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.probabilityStateEquiv (B : Type u) [BooleanAlgebra B] : ProbabilityPoint B ≃ PositiveState B

Finitely additive probabilities and positive normalized states on EventSpan are canonically equivalent.

Equations

• One or more equations did not get rendered due to their size.