Grace/Cumulus/FixedPoint/KuhnSimplex.g17

Open in Workbench Download source

Imports

Set · Set.Indicator · Cardinal.IndicatorSum

Declarations

Source

1-- Kuhn simplices: the cells of the standard triangulation of the cube2-- {0, …, p}ⁿ. A simplex is determined by a base point and an order upd on3-- the coordinates; its vertices step from the base one coordinate at a4-- time in that order.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.FixedPoint.KuhnSimplex11import Set12import Set.Indicator13import Cardinal.IndicatorSum1415-- The i-th vertex raises the coordinates upd(0), …, upd(i − 1) by one.16def raised (n upd i : Set) : Set := functionImage(upd, i, n)1718defgraph kuhnPoint (n base upd i : Set) (j ∈ n) : ℕ := base(j) + indicator(raised(n, upd, i), j)19requires baseFunction : base : n → ℕ20proof21  have value := FunctionBetween.apply_closed with baseFunction, assumption22  have valueNat := nat.omega.backward with value23  have tag := indicator.natural at raised(n, upd, i), j24  have sumNat : Nat(base(j) + indicator(raised(n, upd, i), j)) by typecheck25  exact nat.omega.forward with sumNat2627defgraph kuhnVertex (n base upd : Set) (i ∈ succ(n)) : functionSpace(n, ℕ) := kuhnPoint(n, base, upd, i)28requires baseFunction : base : n → ℕ29proof30  have function := kuhnPoint.function at n, base, upd, i with baseFunction31  exact functionSpace.mem_iff.backward with function3233def kuhnSimplex (n base upd : Set) : Set :=34  functionImage(kuhnVertex(n, base, upd), succ(n), functionSpace(n, ℕ))3536predicate KuhnSimplex (p n s : Set) :=37  ∃ base ∈ functionSpace(n, ℕ), (∀ j ∈ n, base(j) < p) ∧38    ∃ upd, BijectiveBetween(upd, n, n) ∧ s = kuhnSimplex(n, base, upd)3940theorem raised.membership (j n upd i : Set)41  shows j ∈ raised(n, upd, i) ↔ j ∈ n ∧ ∃ k ∈ i, j = upd(k)42proof43  have same : raised(n, upd, i) = functionImage(upd, i, n)44    unfold raised45    rfl46  rw same47  exact functionImage.membership4849theorem kuhnSimplex.membership (x n base upd : Set)50  shows x ∈ kuhnSimplex(n, base, upd) ↔ x ∈ functionSpace(n, ℕ) ∧ ∃ i ∈ succ(n), x = kuhnVertex(n, base, upd)(i)51proof52  have same : kuhnSimplex(n, base, upd) = functionImage(kuhnVertex(n, base, upd), succ(n), functionSpace(n, ℕ))53    unfold kuhnSimplex54    rfl55  rw same56  exact functionImage.membership5758theorem kuhnVertex.coordinate (n base upd i j : Set)59  requires baseFunction : base : n → ℕ60  requires hi : i ∈ succ(n)61  requires hj : j ∈ n62  shows kuhnVertex(n, base, upd)(i)(j) = base(j) + indicator(raised(n, upd, i), j)63proof64  have vertex := kuhnVertex.value at n, base, upd, i with baseFunction65  have point := kuhnPoint.value at n, base, upd, i, j with baseFunction66  rw [vertex, point]67  rfl6869-- Raised coordinate sets grow one coordinate at a time.70theorem raised.monotone (n upd i k : Set)71  requires hik : i ⊆ k72  shows raised(n, upd, i) ⊆ raised(n, upd, k)73proof74  intros j hj75  obtain ⟨hjn, x, hx, shape⟩ := raised.membership.forward with hj76  exact raised.membership.backward with ⟨hjn, x, (hik with x, hx), shape⟩7778theorem raised.succ (n : Nat) (upd i : Set)79  requires updFunction : upd : n → n80  requires hi : i ∈ n81  shows raised(n, upd, succ(i)) = insert(upd(i), raised(n, upd, i))82proof83  have naturals := natural.member at n84  have iNat := naturals with hi85  have value := FunctionBetween.apply_closed with updFunction, hi86  ext j87  constructor88  . intro hj89    obtain ⟨hjn, k, hk, shape⟩ := raised.membership.forward with hj90    have split := bootstrap.succ.membership.forward with hk91    apply insert.membership.backward92    cases split with before | same93    . right94      exact raised.membership.backward with ⟨hjn, k, before, shape⟩95    . left96      rw [shape, same]97      rfl98  . intro hj99    have split := insert.membership.forward with hj100    cases split with same | inRaised101    . rw same102      have self := bootstrap.succ.self at i103      exact raised.membership.backward with ⟨value, i, self, rfl⟩104    . obtain ⟨hjn, k, hk, shape⟩ := raised.membership.forward with inRaised105      have later := membership.into_successor with hk106      exact raised.membership.backward with ⟨hjn, k, later, shape⟩107108theorem raised.fresh (n : Nat) (upd i : Set)109  requires injective : InjectiveBetween(upd, n, n)110  requires hi : i ∈ n111  shows ¬upd(i) ∈ raised(n, upd, i)112proof113  intro inside114  obtain ⟨hjn, k, hk, shape⟩ := raised.membership.forward with inside115  have below := Ordinal.member_subset with hi116  have hkn := below with k, hk117  have same := Injective.apply_cancel with injective, hi, hkn, shape118  rw same at hk119  have irreflexive := Ordinal.not_member_self at k120  exact irreflexive with hk121122theorem raised.subset (n upd i : Set)123  shows raised(n, upd, i) ⊆ n124proof125  intros j hj126  obtain ⟨hjn, k, hk, shape⟩ := raised.membership.forward with hj127  exact hjn128129-- Vertices.130theorem kuhnVertex.member (n base upd i : Set)131  requires baseFunction : base : n → ℕ132  requires hi : i ∈ succ(n)133  shows kuhnVertex(n, base, upd)(i) ∈ kuhnSimplex(n, base, upd)134proof135  have graph := kuhnVertex.function at n, base, upd with baseFunction136  have closed := FunctionBetween.apply_closed with graph, hi137  exact kuhnSimplex.membership.backward with ⟨closed, i, hi, rfl⟩138139theorem kuhnVertex.function_on (n base upd i : Set)140  requires baseFunction : base : n → ℕ141  requires hi : i ∈ succ(n)142  shows kuhnVertex(n, base, upd)(i) : n → ℕ143proof144  have graph := kuhnVertex.function at n, base, upd with baseFunction145  have closed := FunctionBetween.apply_closed with graph, hi146  exact functionSpace.mem_iff.forward with closed147148theorem kuhnVertex.coordinate_succ (n : Nat) (base upd i j : Set)149  requires baseFunction : base : n → ℕ150  requires updInjective : InjectiveBetween(upd, n, n)151  requires hi : i ∈ n152  requires hj : j ∈ n153  shows kuhnVertex(n, base, upd)(succ(i))(j) = kuhnVertex(n, base, upd)(i)(j) + indicator({upd(i)}, j)154proof155  have updFunction := Injective.function with updInjective156  have naturals := natural.member at n157  have iNat := naturals with hi158  have below := Less.of_membership with hi159  have succBelow : succ(i) < succ(n) by arith160  have succIn := membership.of_Less with succBelow161  have iIn := membership.into_successor with hi162  have first := kuhnVertex.coordinate at n, base, upd, succ(i), j with baseFunction, succIn, hj163  have second := kuhnVertex.coordinate at n, base, upd, i, j with baseFunction, iIn, hj164  have step := raised.succ with updFunction, hi165  have baseValue := FunctionBetween.apply_closed with baseFunction, hj166  have baseNat := nat.omega.backward with baseValue167  rw [first, second, step]168  have split : j = upd(i) ∨ j ≠ upd(i) by tauto169  cases split with same | different170  . have inInsert : j ∈ insert(upd(i), raised(n, upd, i))171      apply insert.membership.backward172      left173      exact same174    have single : j ∈ {upd(i)} := singleton.membership.backward with same175    have fresh := raised.fresh with updInjective, hi176    have absent : ¬j ∈ raised(n, upd, i) by rwa same177    have one := indicator.member with inInsert178    have zero := indicator.absent with absent179    have one2 := indicator.member with single180    rw [one, zero, one2]181    rw add.right_unit182    rfl183  . have equivalent : j ∈ insert(upd(i), raised(n, upd, i)) ↔ j ∈ raised(n, upd, i)184      constructor185      . intro inside186        have split2 := insert.membership.forward with inside187        cases split2 with same | inRaised188        . exfalso189          exact different with same190        . exact inRaised191      . intro inRaised192        apply insert.membership.backward193        right194        exact inRaised195    have different2 : upd(i) ≠ j196      intro same197      apply different198      symm199      exact same200    have congr := indicator.congr with equivalent201    have zero := indicator.singleton_other with different2202    rw [congr, zero]203    rw add.right_unit204    rfl205206-- Monotonicity along the vertex chain, and strictness at the raised207-- coordinate.208theorem indicator.monotone (A B j : Set)209  requires hAB : A ⊆ B210  shows indicator(A, j) ≤ indicator(B, j)211proof212  have split : j ∈ A ∨ ¬j ∈ A by tauto213  cases split with inA | outA214  . have inB := hAB with j, inA215    have oneA := indicator.member with inA216    have oneB := indicator.member with inB217    rw [oneA, oneB]218    arith219  . have zero := indicator.absent with outA220    rw zero221    arith222223theorem kuhnVertex.monotone (n : Nat) (base upd i k j : Set)224  requires baseFunction : base : n → ℕ225  requires hi : i ∈ succ(n)226  requires hk : k ∈ succ(n)227  requires hik : i ⊆ k228  requires hj : j ∈ n229  shows kuhnVertex(n, base, upd)(i)(j) ≤ kuhnVertex(n, base, upd)(k)(j)230proof231  have first := kuhnVertex.coordinate at n, base, upd, i, j with baseFunction, hi, hj232  have second := kuhnVertex.coordinate at n, base, upd, k, j with baseFunction, hk, hj233  have grown := raised.monotone at n, upd, i, k with hik234  have tags := indicator.monotone at raised(n, upd, i), raised(n, upd, k), j with grown235  have baseValue := FunctionBetween.apply_closed with baseFunction, hj236  have baseNat := nat.omega.backward with baseValue237  rw [first, second]238  arith239240theorem kuhnVertex.strict (n : Nat) (base upd i k : Set)241  requires baseFunction : base : n → ℕ242  requires updInjective : InjectiveBetween(upd, n, n)243  requires hi : i ∈ n244  requires hk : k ∈ succ(n)245  requires hik : i ∈ k246  shows kuhnVertex(n, base, upd)(i)(upd(i)) < kuhnVertex(n, base, upd)(k)(upd(i))247proof248  have updFunction := Injective.function with updInjective249  have value := FunctionBetween.apply_closed with updFunction, hi250  have iIn := membership.into_successor with hi251  have first := kuhnVertex.coordinate at n, base, upd, i, upd(i) with baseFunction, iIn, value252  have second := kuhnVertex.coordinate at n, base, upd, k, upd(i) with baseFunction, hk, value253  have fresh := raised.fresh with updInjective, hi254  have inK : upd(i) ∈ raised(n, upd, k) := raised.membership.backward with ⟨value, i, hik, rfl⟩255  have zero := indicator.absent with fresh256  have one := indicator.member with inK257  have baseValue := FunctionBetween.apply_closed with baseFunction, value258  have baseNat := nat.omega.backward with baseValue259  rw [first, second, zero, one]260  arith261262theorem kuhnVertex.injective (n : Nat) (base upd i k : Set)263  requires baseFunction : base : n → ℕ264  requires updInjective : InjectiveBetween(upd, n, n)265  requires hi : i ∈ succ(n)266  requires hk : k ∈ succ(n)267  requires equal : kuhnVertex(n, base, upd)(i) = kuhnVertex(n, base, upd)(k)268  shows i = k269proof270  have naturals := natural.member at succ(n)271  have iNat := naturals with hi272  have kNat := naturals with hk273  have order := Ordinal.trichotomy with (Ordinal.natural at i), k, (Ordinal.natural at k)274  cases order with below | rest275  . exfalso276    have iInN : i ∈ n277      have below2 := Less.of_membership with below278      have kBound := Less.of_membership with hk279      have small : i < n by arith280      exact membership.of_Less with small281    have strict := kuhnVertex.strict with baseFunction, updInjective, iInN, hk, below282    rw equal at strict283    have updFunction := Injective.function with updInjective284    have coordinate := FunctionBetween.apply_closed with updFunction, iInN285    have vertexFunction := kuhnVertex.function_on at n, base, upd, k with baseFunction, hk286    have valueIn := FunctionBetween.apply_closed with vertexFunction, coordinate287    have valueNat := nat.omega.backward with valueIn288    exact Less.irreflexive with strict289  . cases rest with same | above290    . exact same291    . exfalso292      have kInN : k ∈ n293        have above2 := Less.of_membership with above294        have iBound := Less.of_membership with hi295        have small : k < n by arith296        exact membership.of_Less with small297      have strict := kuhnVertex.strict with baseFunction, updInjective, kInN, hi, above298      rw equal at strict299      have updFunction := Injective.function with updInjective300      have coordinate := FunctionBetween.apply_closed with updFunction, kInN301      have vertexFunction := kuhnVertex.function_on at n, base, upd, k with baseFunction, hk302      have valueIn := FunctionBetween.apply_closed with vertexFunction, coordinate303      have valueNat := nat.omega.backward with valueIn304      exact Less.irreflexive with strict305306theorem kuhnVertex.graph_injective (n : Nat) (base upd : Set)307  requires baseFunction : base : n → ℕ308  requires updInjective : InjectiveBetween(upd, n, n)309  shows InjectiveBetween(kuhnVertex(n, base, upd), succ(n), functionSpace(n, ℕ))310proof311  have graph := kuhnVertex.function at n, base, upd with baseFunction312  constructor313  . exact graph314  . intros i hi k hk z hz hiz hkz315    have valueI := FunctionBetween.apply_value with graph, hi, hiz316    have valueK := FunctionBetween.apply_value with graph, hk, hkz317    have equal : kuhnVertex(n, base, upd)(i) = kuhnVertex(n, base, upd)(k) by cc318    exact kuhnVertex.injective with baseFunction, updInjective, hi, hk, equal319320theorem kuhnSimplex.cardinality (n : Nat) (base upd : Set)321  requires baseFunction : base : n → ℕ322  requires updInjective : InjectiveBetween(upd, n, n)323  shows cardinality(kuhnSimplex(n, base, upd)) = succ(n)324proof325  have injective := kuhnVertex.graph_injective with baseFunction, updInjective326  have corestricted := Injective.corestrict with injective327  have surjective := functionImage.surjective with (Injective.function with injective)328  have bijective : BijectiveBetween(kuhnVertex(n, base, upd), succ(n), functionImage(kuhnVertex(n, base, upd), succ(n), functionSpace(n, ℕ))) := ⟨corestricted, surjective⟩329  have same := cardinality.bijective with bijective330  have count := cardinality.natural at succ(n)331  unfold kuhnSimplex332  rw [← same, count]333  rfl334335theorem kuhnSimplex.finite (n : Nat) (base upd : Set)336  requires baseFunction : base : n → ℕ337  requires updInjective : InjectiveBetween(upd, n, n)338  shows Finite(kuhnSimplex(n, base, upd))339proof340  have injective := kuhnVertex.graph_injective with baseFunction, updInjective341  have corestricted := Injective.corestrict with injective342  have surjective := functionImage.surjective with (Injective.function with injective)343  have bijective : BijectiveBetween(kuhnVertex(n, base, upd), succ(n), functionImage(kuhnVertex(n, base, upd), succ(n), functionSpace(n, ℕ))) := ⟨corestricted, surjective⟩344  have equipotent : succ(n) ≃ functionImage(kuhnVertex(n, base, upd), succ(n), functionSpace(n, ℕ)) := ⟨kuhnVertex(n, base, upd), bijective⟩345  unfold kuhnSimplex346  exact Finite.of_equipotent with (Finite.natural at succ(n)), equipotent347348-- Bounds on the coordinates.349theorem kuhnVertex.between (n : Nat) (base upd i j : Set)350  requires baseFunction : base : n → ℕ351  requires hi : i ∈ succ(n)352  requires hj : j ∈ n353  shows base(j) ≤ kuhnVertex(n, base, upd)(i)(j) ∧ kuhnVertex(n, base, upd)(i)(j) ≤ base(j) + 1354proof355  have value := kuhnVertex.coordinate at n, base, upd, i, j with baseFunction, hi, hj356  have baseValue := FunctionBetween.apply_closed with baseFunction, hj357  have baseNat := nat.omega.backward with baseValue358  rw value359  have split : j ∈ raised(n, upd, i) ∨ ¬j ∈ raised(n, upd, i) by tauto360  cases split with inside | outside361  . have one := indicator.member with inside362    rw one363    constructor364    . arith365    . arith366  . have zero := indicator.absent with outside367    rw zero368    constructor369    . arith370    . arith371372theorem kuhnVertex.bounded (n : Nat) (base upd i j p : Set)373  requires baseFunction : base : n → ℕ374  requires pNat : Nat(p)375  requires below : base(j) < p376  requires hi : i ∈ succ(n)377  requires hj : j ∈ n378  shows kuhnVertex(n, base, upd)(i)(j) ≤ p379proof380  have bounds := kuhnVertex.between at n, base, upd, i, j with baseFunction, hi, hj381  have baseValue := FunctionBetween.apply_closed with baseFunction, hj382  have baseNat := nat.omega.backward with baseValue383  have upper := bounds.right384  have vertexFunction := kuhnVertex.function_on at n, base, upd, i with baseFunction, hi385  have valueIn := FunctionBetween.apply_closed with vertexFunction, hj386  have valueNat := nat.omega.backward with valueIn387  arith388389-- The first vertex is the base; the last raises every coordinate.390theorem raised.zero (n upd : Set)391  shows raised(n, upd, 0) = ∅392proof393  have same : raised(n, upd, 0) = functionImage(upd, 0, n)394    unfold raised395    rfl396  rw [same, nat.zero]397  exact functionImage.empty398399theorem raised.full (n upd : Set)400  requires bijective : BijectiveBetween(upd, n, n)401  shows raised(n, upd, n) = n402proof403  have function := Injective.function with (Bijective.injective with bijective)404  have surjective := Bijective.surjective with bijective405  apply Subset.antisymmetric406  . exact raised.subset at n, upd, n407  . intros j hj408    obtain ⟨k, hk, related⟩ := surjective.right with j, hj409    have value := FunctionBetween.apply_value with function, hk, related410    apply raised.membership.backward411    refine ⟨hj, k, hk, ?_⟩412    symm413    exact value414415theorem kuhnVertex.zero_coordinate (n : Nat) (base upd j : Set)416  requires baseFunction : base : n → ℕ417  requires hj : j ∈ n418  shows kuhnVertex(n, base, upd)(0)(j) = base(j)419proof420  have zeroNat : Nat(0) by typecheck421  have positive : 0 < succ(n) by arith422  have zeroIn := membership.of_Less with positive423  have value := kuhnVertex.coordinate at n, base, upd, 0, j with baseFunction, zeroIn, hj424  have absent : ¬j ∈ ∅425    intro inside426    exact empty.membership with j, inside427  have zero := indicator.absent with absent428  have baseValue := FunctionBetween.apply_closed with baseFunction, hj429  have baseNat := nat.omega.backward with baseValue430  rw [value, raised.zero, zero, add.right_unit]431  rfl432433theorem kuhnVertex.top_coordinate (n : Nat) (base upd j : Set)434  requires baseFunction : base : n → ℕ435  requires bijective : BijectiveBetween(upd, n, n)436  requires hj : j ∈ n437  shows kuhnVertex(n, base, upd)(n)(j) = base(j) + 1438proof439  have nIn := bootstrap.succ.self at n440  have value := kuhnVertex.coordinate at n, base, upd, n, j with baseFunction, nIn, hj441  have full := raised.full with bijective442  have one := indicator.member with hj443  rw [value, full, one]444  rfl445446-- Any two vertices are comparable coordinatewise.447theorem kuhnVertex.comparable (n : Nat) (base upd i k j : Set)448  requires baseFunction : base : n → ℕ449  requires hi : i ∈ succ(n)450  requires hk : k ∈ succ(n)451  requires hj : j ∈ n452  shows kuhnVertex(n, base, upd)(i)(j) ≤ kuhnVertex(n, base, upd)(k)(j) ∨453    kuhnVertex(n, base, upd)(k)(j) ≤ kuhnVertex(n, base, upd)(i)(j)454proof455  have naturals := natural.member at succ(n)456  have iNat := naturals with hi457  have kNat := naturals with hk458  have order := Ordinal.trichotomy with (Ordinal.natural at i), k, (Ordinal.natural at k)459  cases order with below | rest460  . left461    have hik := Ordinal.member_subset with (Ordinal.natural at k), below462    exact kuhnVertex.monotone with baseFunction, hi, hk, hik, hj463  . cases rest with same | above464    . left465      rw same466      have vertexFunction := kuhnVertex.function_on at n, base, upd, k with baseFunction, hk467      have valueIn := FunctionBetween.apply_closed with vertexFunction, hj468      have valueNat := nat.omega.backward with valueIn469      arith470    . right471      have hki := Ordinal.member_subset with (Ordinal.natural at i), above472      exact kuhnVertex.monotone with baseFunction, hk, hi, hki, hj473474-- Vertices agree once their coordinates do.475theorem kuhnVertex.ext (n : Nat) (base upd i k : Set)476  requires baseFunction : base : n → ℕ477  requires hi : i ∈ succ(n)478  requires hk : k ∈ succ(n)479  requires same : ∀ j ∈ n, kuhnVertex(n, base, upd)(i)(j) = kuhnVertex(n, base, upd)(k)(j)480  shows kuhnVertex(n, base, upd)(i) = kuhnVertex(n, base, upd)(k)481proof482  have fi := kuhnVertex.function_on at n, base, upd, i with baseFunction, hi483  have fk := kuhnVertex.function_on at n, base, upd, k with baseFunction, hk484  exact FunctionBetween.ext with fi, fk, same485486theorem kuhnVertex.index_subset (n : Nat) (i : Set)487  requires hi : i ∈ succ(n)488  shows i ⊆ n489proof490  have split := bootstrap.succ.membership.forward with hi491  cases split with below | same492  . exact Ordinal.member_subset with (Ordinal.natural at n), below493  . rw same494    exact Subset.reflexive495496-- The last vertex lies above every vertex; the first lies below.497theorem kuhnVertex.top_of_face (n : Nat) (base upd x j : Set)498  requires baseFunction : base : n → ℕ499  requires hx : x ∈ kuhnSimplex(n, base, upd)500  requires hj : j ∈ n501  shows x(j) ≤ kuhnVertex(n, base, upd)(n)(j)502proof503  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with hx504  have hin := kuhnVertex.index_subset with hi505  have nIn := bootstrap.succ.self at n506  rw shape507  exact kuhnVertex.monotone with baseFunction, hi, nIn, hin, hj508509theorem kuhnVertex.bottom_of_face (n : Nat) (base upd x j : Set)510  requires baseFunction : base : n → ℕ511  requires hx : x ∈ kuhnSimplex(n, base, upd)512  requires hj : j ∈ n513  shows kuhnVertex(n, base, upd)(0)(j) ≤ x(j)514proof515  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with hx516  have positive : 0 < succ(n) by arith517  have zeroIn := membership.of_Less with positive518  have zeroSub : 0 ⊆ i519    rw nat.zero520    exact empty.subset521  rw shape522  exact kuhnVertex.monotone with baseFunction, zeroIn, hi, zeroSub, hj523524theorem kuhnVertex.top_ne_bottom (n : Nat) (base upd : Set)525  requires baseFunction : base : n → ℕ526  requires updInjective : InjectiveBetween(upd, n, n)527  requires positive : 0 ∈ n528  shows kuhnVertex(n, base, upd)(n) ≠ kuhnVertex(n, base, upd)(0)529proof530  intro equal531  have zeroIn := membership.into_successor with positive532  have nIn := bootstrap.succ.self at n533  have same := kuhnVertex.injective with baseFunction, updInjective, nIn, zeroIn, equal534  rw same at positive535  have irreflexive := Ordinal.not_member_self at 0536  exact irreflexive with positive537538-- A face determines the missing vertex: below the bottom vertex the face's539-- maximum is the top vertex, and above the top vertex its minimum is the540-- bottom vertex.541theorem kuhnSimplex.top_of_bottom_face (n : Nat) (base upd M : Set)542  requires baseFunction : base : n → ℕ543  requires updInjective : InjectiveBetween(upd, n, n)544  requires positive : 0 ∈ n545  requires hM : M ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}546  requires maximal : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}, ∀ j ∈ n, x(j) ≤ M(j)547  shows M = kuhnVertex(n, base, upd)(n)548proof549  have nIn := bootstrap.succ.self at n550  have topMember := kuhnVertex.member at n, base, upd, n with baseFunction, nIn551  have topDifferent := kuhnVertex.top_ne_bottom with baseFunction, updInjective, positive552  have topInFace : kuhnVertex(n, base, upd)(n) ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}553    exact difference.singleton_membership.backward with ⟨topMember, topDifferent⟩554  have parts := difference.singleton_membership.forward with hM555  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with parts.left556  have below := maximal with kuhnVertex(n, base, upd)(n), topInFace557  rw shape558  apply kuhnVertex.ext with baseFunction, hi, nIn559  intros j hj560  have above := kuhnVertex.top_of_face with baseFunction, parts.left, hj561  have belowJ := below with hj562  rw shape at above563  rw shape at belowJ564  have vi := kuhnVertex.function_on at n, base, upd, i with baseFunction, hi565  have vn := kuhnVertex.function_on at n, base, upd, n with baseFunction, nIn566  have valueI := nat.omega.backward with (FunctionBetween.apply_closed with vi, hj)567  have valueN := nat.omega.backward with (FunctionBetween.apply_closed with vn, hj)568  exact LessEqual.antisymmetric with above, belowJ569570theorem kuhnSimplex.bottom_of_top_face (n : Nat) (base upd M : Set)571  requires baseFunction : base : n → ℕ572  requires updInjective : InjectiveBetween(upd, n, n)573  requires positive : 0 ∈ n574  requires hM : M ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}575  requires minimal : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}, ∀ j ∈ n, M(j) ≤ x(j)576  shows M = kuhnVertex(n, base, upd)(0)577proof578  have zeroNat : Nat(0) by typecheck579  have zeroIn := membership.into_successor with positive580  have nIn := bootstrap.succ.self at n581  have bottomMember := kuhnVertex.member at n, base, upd, 0 with baseFunction, zeroIn582  have topDifferent := kuhnVertex.top_ne_bottom with baseFunction, updInjective, positive583  have bottomDifferent : kuhnVertex(n, base, upd)(0) ≠ kuhnVertex(n, base, upd)(n)584    intro equal585    apply topDifferent586    symm587    exact equal588  have bottomInFace : kuhnVertex(n, base, upd)(0) ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}589    exact difference.singleton_membership.backward with ⟨bottomMember, bottomDifferent⟩590  have parts := difference.singleton_membership.forward with hM591  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with parts.left592  have above := minimal with kuhnVertex(n, base, upd)(0), bottomInFace593  rw shape594  apply kuhnVertex.ext with baseFunction, hi, zeroIn595  intros j hj596  have below := kuhnVertex.bottom_of_face with baseFunction, parts.left, hj597  have aboveJ := above with hj598  rw shape at below599  rw shape at aboveJ600  have vi := kuhnVertex.function_on at n, base, upd, i with baseFunction, hi601  have v0 := kuhnVertex.function_on at n, base, upd, 0 with baseFunction, zeroIn602  have valueI := nat.omega.backward with (FunctionBetween.apply_closed with vi, hj)603  have value0 := nat.omega.backward with (FunctionBetween.apply_closed with v0, hj)604  exact LessEqual.antisymmetric with aboveJ, below605606-- Two simplices sharing the face below their bottom vertices coincide.607theorem kuhnSimplex.eq_bottom (n : Nat) (b1 u1 b2 u2 : Set)608  requires f1 : b1 : n → ℕ609  requires bij1 : BijectiveBetween(u1, n, n)610  requires f2 : b2 : n → ℕ611  requires bij2 : BijectiveBetween(u2, n, n)612  requires positive : 0 ∈ n613  requires same : kuhnSimplex(n, b1, u1) ∖ {kuhnVertex(n, b1, u1)(0)} = kuhnSimplex(n, b2, u2) ∖ {kuhnVertex(n, b2, u2)(0)}614  shows kuhnSimplex(n, b1, u1) = kuhnSimplex(n, b2, u2)615proof616  have inj1 := Bijective.injective with bij1617  have inj2 := Bijective.injective with bij2618  have zeroNat : Nat(0) by typecheck619  have zeroIn := membership.into_successor with positive620  have nIn := bootstrap.succ.self at n621  have top1Member := kuhnVertex.member at n, b1, u1, n with f1, nIn622  have top1Different := kuhnVertex.top_ne_bottom with f1, inj1, positive623  have top1InFace : kuhnVertex(n, b1, u1)(n) ∈ kuhnSimplex(n, b1, u1) ∖ {kuhnVertex(n, b1, u1)(0)}624    exact difference.singleton_membership.backward with ⟨top1Member, top1Different⟩625  have maximal1 : ∀ x ∈ kuhnSimplex(n, b1, u1) ∖ {kuhnVertex(n, b1, u1)(0)}, ∀ j ∈ n, x(j) ≤ kuhnVertex(n, b1, u1)(n)(j)626    intros x hx j hj627    have parts := difference.singleton_membership.forward with hx628    exact kuhnVertex.top_of_face with f1, parts.left, hj629  rw same at top1InFace630  rw under same at maximal1631  have topsEqual := kuhnSimplex.top_of_bottom_face with f2, inj2, positive, top1InFace, maximal1632  have basesEqual : b1 = b2633    apply FunctionBetween.ext with f1, f2634    intros j hj635    have t1 := kuhnVertex.top_coordinate with f1, bij1, hj636    have t2 := kuhnVertex.top_coordinate with f2, bij2, hj637    rw topsEqual at t1638    have equal : b1(j) + 1 = b2(j) + 1 by cc639    have v1 := nat.omega.backward with (FunctionBetween.apply_closed with f1, hj)640    have v2 := nat.omega.backward with (FunctionBetween.apply_closed with f2, hj)641    have oneNat : Nat(1) by typecheck642    exact add.right_cancel with equal643  have bottomsEqual : kuhnVertex(n, b1, u1)(0) = kuhnVertex(n, b2, u2)(0)644    have g1 := kuhnVertex.function_on at n, b1, u1, 0 with f1, zeroIn645    have g2 := kuhnVertex.function_on at n, b2, u2, 0 with f2, zeroIn646    apply FunctionBetween.ext with g1, g2647    intros j hj648    have z1 := kuhnVertex.zero_coordinate at n, b1, u1, j with f1, hj649    have z2 := kuhnVertex.zero_coordinate at n, b2, u2, j with f2, hj650    rw [z1, z2, basesEqual]651    rfl652  have bottom1Member := kuhnVertex.member at n, b1, u1, 0 with f1, zeroIn653  have bottom2Member := kuhnVertex.member at n, b2, u2, 0 with f2, zeroIn654  have restore1 := insert.restore with bottom1Member655  have restore2 := insert.restore with bottom2Member656  rwa [← restore1, same, bottomsEqual]657658-- Two simplices sharing the face above their top vertices coincide.659theorem kuhnSimplex.eq_top (n : Nat) (b1 u1 b2 u2 : Set)660  requires f1 : b1 : n → ℕ661  requires bij1 : BijectiveBetween(u1, n, n)662  requires f2 : b2 : n → ℕ663  requires bij2 : BijectiveBetween(u2, n, n)664  requires positive : 0 ∈ n665  requires same : kuhnSimplex(n, b1, u1) ∖ {kuhnVertex(n, b1, u1)(n)} = kuhnSimplex(n, b2, u2) ∖ {kuhnVertex(n, b2, u2)(n)}666  shows kuhnSimplex(n, b1, u1) = kuhnSimplex(n, b2, u2)667proof668  have inj1 := Bijective.injective with bij1669  have inj2 := Bijective.injective with bij2670  have zeroNat : Nat(0) by typecheck671  have zeroIn := membership.into_successor with positive672  have nIn := bootstrap.succ.self at n673  have bottom1Member := kuhnVertex.member at n, b1, u1, 0 with f1, zeroIn674  have top1Different := kuhnVertex.top_ne_bottom with f1, inj1, positive675  have bottom1Different : kuhnVertex(n, b1, u1)(0) ≠ kuhnVertex(n, b1, u1)(n)676    intro equal677    apply top1Different678    symm679    exact equal680  have bottom1InFace : kuhnVertex(n, b1, u1)(0) ∈ kuhnSimplex(n, b1, u1) ∖ {kuhnVertex(n, b1, u1)(n)}681    exact difference.singleton_membership.backward with ⟨bottom1Member, bottom1Different⟩682  have minimal1 : ∀ x ∈ kuhnSimplex(n, b1, u1) ∖ {kuhnVertex(n, b1, u1)(n)}, ∀ j ∈ n, kuhnVertex(n, b1, u1)(0)(j) ≤ x(j)683    intros x hx j hj684    have parts := difference.singleton_membership.forward with hx685    exact kuhnVertex.bottom_of_face with f1, parts.left, hj686  rw same at bottom1InFace687  rw under same at minimal1688  have bottomsEqual := kuhnSimplex.bottom_of_top_face with f2, inj2, positive, bottom1InFace, minimal1689  have basesEqual : b1 = b2690    apply FunctionBetween.ext with f1, f2691    intros j hj692    have z1 := kuhnVertex.zero_coordinate at n, b1, u1, j with f1, hj693    have z2 := kuhnVertex.zero_coordinate at n, b2, u2, j with f2, hj694    rw bottomsEqual at z1695    cc696  have topsEqual : kuhnVertex(n, b1, u1)(n) = kuhnVertex(n, b2, u2)(n)697    have g1 := kuhnVertex.function_on at n, b1, u1, n with f1, nIn698    have g2 := kuhnVertex.function_on at n, b2, u2, n with f2, nIn699    apply FunctionBetween.ext with g1, g2700    intros j hj701    have t1 := kuhnVertex.top_coordinate with f1, bij1, hj702    have t2 := kuhnVertex.top_coordinate with f2, bij2, hj703    rw [t1, t2, basesEqual]704    rfl705  have top1Member := kuhnVertex.member at n, b1, u1, n with f1, nIn706  have top2Member := kuhnVertex.member at n, b2, u2, n with f2, nIn707  have restore1 := insert.restore with top1Member708  have restore2 := insert.restore with top2Member709  rwa [← restore1, same, topsEqual]710711-- The coordinate sum of the k-th vertex exceeds that of the base by k,712-- so a vertex is determined by its sum.713theorem raised.cardinality (n : Nat) (upd k : Set)714  requires updInjective : InjectiveBetween(upd, n, n)715  requires hk : k ∈ succ(n)716  shows cardinality(raised(n, upd, k)) = k717proof718  have naturals := natural.member at succ(n)719  have kNat := naturals with hk720  have inside := kuhnVertex.index_subset with hk721  have same : raised(n, upd, k) = functionImage(upd, k, n)722    unfold raised723    rfl724  rw same725  have count := cardinality.injective_image with updInjective, inside, (Finite.natural at k)726  rw count727  exact cardinality.natural728729theorem kuhnVertex.sum (n : Nat) (base upd k : Set)730  requires baseFunction : base : n → ℕ731  requires updInjective : InjectiveBetween(upd, n, n)732  requires hk : k ∈ succ(n)733  shows natSum(n, kuhnVertex(n, base, upd)(k)) = natSum(n, base) + k734proof735  have finite := Finite.natural at n736  have size : cardinality(n) = n := cardinality.natural737  have baseWeights : ∀ j ∈ n, base(j) ∈ ℕ738    intros j hj739    exact FunctionBetween.apply_closed with baseFunction, hj740  have tagGraph := indicatorMap.function at raised(n, upd, k), n741  have tagWeights : ∀ j ∈ n, indicatorMap(raised(n, upd, k), n)(j) ∈ ℕ742    intros j hj743    exact FunctionBetween.apply_closed with tagGraph, hj744  have agree : ∀ j ∈ n, kuhnVertex(n, base, upd)(k)(j) = base(j) + indicatorMap(raised(n, upd, k), n)(j)745    intros j hj746    have value := kuhnVertex.coordinate at n, base, upd, k, j with baseFunction, hk, hj747    have tag := indicatorMap.value at raised(n, upd, k), n, j with hj748    rw [value, tag]749    rfl750  have additive := natSum.add_pointwise_of_size at kuhnVertex(n, base, upd)(k), base, indicatorMap(raised(n, upd, k), n), n751  have split := additive with n, finite, size, baseWeights, tagWeights, agree752  have counted := natSum.indicator_of_size at raised(n, upd, k), n753  have tags := counted with n, size754  have inside := raised.subset at n, upd, k755  have intersected : n ∩ raised(n, upd, k) = raised(n, upd, k) := intersection.eq_right_of_subset with inside756  have count := raised.cardinality with updInjective, hk757  rw [split, tags, intersected, count]758  rfl759760theorem kuhnSimplex.sum_of_member (n : Nat) (base upd x : Set)761  requires baseFunction : base : n → ℕ762  requires updInjective : InjectiveBetween(upd, n, n)763  requires hx : x ∈ kuhnSimplex(n, base, upd)764  shows ∃ k ∈ succ(n), x = kuhnVertex(n, base, upd)(k) ∧ natSum(n, x) = natSum(n, base) + k765proof766  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hx767  have total := kuhnVertex.sum with baseFunction, updInjective, hk768  refine ⟨k, hk, shape, ?_⟩769  rwa shape770771theorem kuhnSimplex.sum_determines (n : Nat) (base upd x y : Set)772  requires baseFunction : base : n → ℕ773  requires updInjective : InjectiveBetween(upd, n, n)774  requires hx : x ∈ kuhnSimplex(n, base, upd)775  requires hy : y ∈ kuhnSimplex(n, base, upd)776  requires same : natSum(n, x) = natSum(n, y)777  shows x = y778proof779  obtain ⟨i, hi, shapeX, sumX⟩ := kuhnSimplex.sum_of_member with baseFunction, updInjective, hx780  obtain ⟨k, hk, shapeY, sumY⟩ := kuhnSimplex.sum_of_member with baseFunction, updInjective, hy781  have naturals := natural.member at succ(n)782  have iNat := naturals with hi783  have kNat := naturals with hk784  have baseWeights : ∀ j ∈ n, base(j) ∈ ℕ785    intros j hj786    exact FunctionBetween.apply_closed with baseFunction, hj787  have baseSum := natSum.natural with (Finite.natural at n), baseWeights788  have equal : natSum(n, base) + i = natSum(n, base) + k by cc789  have indices := add.left_cancel with equal790  rw [shapeX, shapeY, indices]791  rfl792793theorem kuhnSimplex.vertex_of_sum (n : Nat) (base upd x k : Set)794  requires baseFunction : base : n → ℕ795  requires updInjective : InjectiveBetween(upd, n, n)796  requires hx : x ∈ kuhnSimplex(n, base, upd)797  requires hk : k ∈ succ(n)798  requires total : natSum(n, x) = natSum(n, base) + k799  shows x = kuhnVertex(n, base, upd)(k)800proof801  have member := kuhnVertex.member at n, base, upd, k with baseFunction, hk802  have vertexSum := kuhnVertex.sum with baseFunction, updInjective, hk803  have same : natSum(n, x) = natSum(n, kuhnVertex(n, base, upd)(k)) by cc804  exact kuhnSimplex.sum_determines with baseFunction, updInjective, hx, member, same805806theorem kuhnSimplex.sum_bounds (n : Nat) (base upd x : Set)807  requires baseFunction : base : n → ℕ808  requires updInjective : InjectiveBetween(upd, n, n)809  requires hx : x ∈ kuhnSimplex(n, base, upd)810  shows natSum(n, base) ≤ natSum(n, x) ∧ natSum(n, x) ≤ natSum(n, base) + n811proof812  obtain ⟨k, hk, shape, total⟩ := kuhnSimplex.sum_of_member with baseFunction, updInjective, hx813  have naturals := natural.member at succ(n)814  have kNat := naturals with hk815  have bound := Less.of_membership with hk816  have baseWeights : ∀ j ∈ n, base(j) ∈ ℕ817    intros j hj818    exact FunctionBetween.apply_closed with baseFunction, hj819  have baseSum := natSum.natural with (Finite.natural at n), baseWeights820  rw total821  constructor822  . arith823  . arith824