PositivePriors.lean

1 import KomorebiLSM.FiniteInstrument
2 
3 /-! Strictly positive beliefs span the entire finite real vector space.
4 The proof uses explicit interior priors rather than an assumed spanning condition. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.FiniteInstruments
7 open scoped BigOperators
8 open FiniteBayes
9 universe u
10 variable {I : Type u} [Fintype I] [Nonempty I]
11 
12 def IsStrictPrior (p : I → ℝ) : Prop := IsPrior p ∧ ∀ i, 0 < p i
13 
14 noncomputable def uniformPrior : I → ℝ := fun _ => (Fintype.card I : ℝ)⁻¹
15 
16 theorem uniform_strict : IsStrictPrior (uniformPrior : I → ℝ) := by
17   have hc : (0 : ℝ) < Fintype.card I := by exact_mod_cast Fintype.card_pos
18   refine ⟨⟨fun _ => (inv_pos.mpr hc).le, ?_⟩, fun _ => inv_pos.mpr hc⟩
19   simp [uniformPrior, ne_of_gt hc]
20 
21 noncomputable def positiveProbe [DecidableEq I] (i : I) : I → ℝ :=
22   (1/2 : ℝ) • uniformPrior + (1/2 : ℝ) • pointMass i
23 
24 theorem positiveProbe_strict [DecidableEq I] (i : I) : IsStrictPrior (positiveProbe i) := by
25   have hu := uniform_strict (I := I)
26   have hp := point_prior i
27   have pos : ∀ j, 0 < positiveProbe i j := by
28     intro j
29     change 0 < (1/2 : ℝ) * uniformPrior j + (1/2 : ℝ) * pointMass i j
30     exact add_pos_of_pos_of_nonneg (mul_pos (by norm_num) (hu.2 j))
31       (mul_nonneg (by norm_num) (hp.1 j))
32   refine ⟨⟨fun j => (pos j).le, ?_⟩, pos⟩
33   simp only [positiveProbe, Pi.add_apply, Pi.smul_apply, smul_eq_mul,
34     Finset.sum_add_distrib, ← Finset.mul_sum, hu.1.2, hp.2]
35   norm_num
36 
37 theorem linearMap_zero_of_strict_priors {E : Type*} [AddCommGroup E] [Module ℝ E]
38     (F : (I → ℝ) →ₗ[ℝ] E)
39     (h : ∀ p, IsStrictPrior p → F p = 0) : F = 0 := by
40   classical
41   have hu := h uniformPrior uniform_strict
42   have hi : ∀ i, F (pointMass i) = 0 := by
43     intro i
44     have hp := h (positiveProbe i) (positiveProbe_strict i)
45     simp only [positiveProbe, map_add, map_smul, hu, smul_zero, zero_add] at hp
46     exact (smul_eq_zero.mp hp).resolve_left (by norm_num)
47   apply LinearMap.ext
48   intro p
49   rw [vector_eq_sum_pointMass p, map_sum]
50   simp only [map_smul, hi, smul_zero, Finset.sum_const_zero, LinearMap.zero_apply]
51 
52 theorem linearMap_eq_of_strict_priors {E : Type*} [AddCommGroup E] [Module ℝ E]
53     (F G : (I → ℝ) →ₗ[ℝ] E)
54     (h : ∀ p, IsStrictPrior p → F p = G p) : F = G := by
55   apply sub_eq_zero.mp
56   exact linearMap_zero_of_strict_priors (F-G) (fun p hp => by simp [h p hp])
57 
58 omit [Nonempty I] in
59 /-- Any nonzero nonnegative branch has positive evidence at every strict belief. -/
60 theorem nonnegative_branch_mass_pos (M : Matrix I I ℝ)
61     (hM : ∀ j i, 0 ≤ M j i) (h0 : M ≠ 0)
62     (p : I → ℝ) (hp : ∀ i, 0 < p i) : 0 < mass (M.mulVecLin p) := by
63   classical
64   obtain ⟨j, i, hji⟩ : ∃ j i, 0 < M j i := by
65     by_contra h
66     push Not at h
67     apply h0
68     ext j i
69     exact le_antisymm (h j i) (hM j i)
70   rw [mass_apply]
71   apply Finset.sum_pos'
72   · intro k _
73     exact Finset.sum_nonneg (fun i _ => mul_nonneg (hM k i) (hp i).le)
74   · refine ⟨j, Finset.mem_univ j, ?_⟩
75     exact Finset.sum_pos' (fun i _ => mul_nonneg (hM j i) (hp i).le)
76       ⟨i, Finset.mem_univ i, mul_pos hji (hp i)⟩
77 
78 end Komorebi.LSM.FiniteInstruments

Back to source controls