Grace/Cumulus/FixedPoint/KuhnFamily.g17

Open in Workbench Download source

Imports

KuhnTopFace · Cardinal.FiniteSubsets

Declarations

Source

1-- The family of all Kuhn simplices of the cube {0, …, p}ⁿ is a finite set2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.FixedPoint.KuhnFamily8import KuhnTopFace9import Cardinal.FiniteSubsets1011def kuhnSimplices (p n : Set) : Set :=12  { s ∈ 𝒫(functionSpace(n, succ(p))) | KuhnSimplex(p, n, s) }1314-- Every vertex of a simplex is a function into {0, …, p}.15theorem kuhnVertex.into_cube (n p : Nat) (base upd i : Set)16  requires baseFunction : base : n → ℕ17  requires bounds : ∀ j ∈ n, base(j) < p18  requires hi : i ∈ succ(n)19  shows kuhnVertex(n, base, upd)(i) ∈ functionSpace(n, succ(p))20proof21  have function := kuhnVertex.function_on at n, base, upd, i with baseFunction, hi22  apply functionSpace.mem_iff.backward23  apply FunctionBetween.codomain_of_values with function24  intros j hj25  have below := bounds with j, hj26  have bounded := kuhnVertex.bounded at n, base, upd, i, j, p with baseFunction, below, hi, hj27  have valueIn := FunctionBetween.apply_closed with function, hj28  have valueNat := nat.omega.backward with valueIn29  have strict : kuhnVertex(n, base, upd)(i)(j) < succ(p) by arith30  exact membership.of_Less with strict3132theorem kuhnSimplex.in_family (n p : Nat) (base upd : Set)33  requires baseFunction : base : n → ℕ34  requires updBijective : BijectiveBetween(upd, n, n)35  requires bounds : ∀ j ∈ n, base(j) < p36  shows kuhnSimplex(n, base, upd) ∈ kuhnSimplices(p, n)37proof38  apply kuhnSimplices.membership.backward39  constructor40  . apply powerset.membership_iff.backward41    intros x hx42    obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with hx43    rw shape44    exact kuhnVertex.into_cube with baseFunction, bounds, hi45  . have baseIn : base ∈ functionSpace(n, ℕ) := functionSpace.mem_iff.backward with baseFunction46    refine ⟨base, baseIn, bounds, upd, updBijective, rfl⟩4748-- The rotation of a simplex stays in the cube as long as its bottom face does49-- not lie on the far wall x_{upd(0)} = p.50theorem kuhnSimplex.rotated_in_family (n p : Nat) (base upd : Set)51  requires baseFunction : base : n → ℕ52  requires updBijective : BijectiveBetween(upd, n, n)53  requires bounds : ∀ j ∈ n, base(j) < p54  requires positive : 0 ∈ n55  requires notFull : ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}, x(upd(0)) ≠ p56  shows kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd)) ∈ kuhnSimplices(p, n)57proof58  have updInjective := Bijective.injective with updBijective59  have updFunction := Injective.function with updInjective60  have jIn := FunctionBetween.apply_closed with updFunction, positive61  have zeroLess := Less.of_membership with positive62  have oneLess : succ(0) < succ(n) by arith63  have oneIn := membership.of_Less with oneLess64  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn65  have rotatedBijective := rotated.bijective with updBijective66  have oneBounds : ∀ j ∈ n, kuhnVertex(n, base, upd)(succ(0))(j) < p67    intros j hj68    have alternatives : j = upd(0) ∨ j ≠ upd(0) by tauto69    cases alternatives with same | different70    . obtain ⟨x, hx, apart⟩ := notFull71      have constant := kuhnSimplex.bottom_face_constant with baseFunction, updBijective, positive, hx72      rw constant at apart73      have below := bounds with jIn74      have bounded := kuhnVertex.bounded at n, base, upd, succ(0), upd(0), p with baseFunction, below, oneIn, jIn75      have valueIn := FunctionBetween.apply_closed with oneFunction, jIn76      have valueNat := nat.omega.backward with valueIn77      have strict : kuhnVertex(n, base, upd)(succ(0))(upd(0)) < succ(p) by arith78      have less := Less.of_successor_upper_ne with strict, apart79      rwa same80    . have value := kuhnVertex.coordinate_succ with baseFunction, updInjective, positive, hj81      have zeroValue := kuhnVertex.zero_coordinate at n, base, upd, j with baseFunction, hj82      have separated : upd(0) ≠ j83        intro equal84        apply different85        symm86        exact equal87      have zero := indicator.singleton_other with separated88      have baseNat := nat.omega.backward with (FunctionBetween.apply_closed with baseFunction, hj)89      have below := bounds with hj90      rw [value, zeroValue, zero]91      arith92  exact kuhnSimplex.in_family with oneFunction, rotatedBijective, oneBounds9394-- The lowering of a simplex stays in the cube: its base is below the old one.95theorem kuhnSimplex.unrotated_in_family (n p : Nat) (base upd m : Set)96  requires baseFunction : base : n → ℕ97  requires updBijective : BijectiveBetween(upd, n, n)98  requires bounds : ∀ j ∈ n, base(j) < p99  requires hm : m ∈ n100  requires top : succ(m) = n101  requires rooted : 0 < base(upd(m))102  shows kuhnSimplex(n, lowered(n, base, upd, m), unrotated(n, upd)) ∈ kuhnSimplices(p, n)103proof104  have lowFunction := lowered.function with baseFunction, rooted105  have unrotatedBijective := unrotated.bijective with updBijective106  have lowBounds : ∀ j ∈ n, lowered(n, base, upd, m)(j) < p107    intros j hj108    have restores := lowered.restores with baseFunction, rooted, hj109    have below := bounds with hj110    have lowNat := nat.omega.backward with (FunctionBetween.apply_closed with lowFunction, hj)111    have baseNat := nat.omega.backward with (FunctionBetween.apply_closed with baseFunction, hj)112    arith113  exact kuhnSimplex.in_family with lowFunction, unrotatedBijective, lowBounds114115theorem kuhnSimplices.finite (n p : Nat)116  shows Finite(kuhnSimplices(p, n))117proof118  have cube : Finite(functionSpace(n, succ(p)))119    have pairs := Finite.product with (Finite.natural at n), (Finite.natural at succ(p))120    have inside : functionSpace(n, succ(p)) ⊆ 𝒫(n × succ(p))121      intros f hf122      have function := functionSpace.mem_iff.forward with hf123      have relation := FunctionBetween.relation with function124      have subset : f ⊆ n × succ(p) := relation125      exact powerset.membership_iff.backward with subset126    exact Finite.subset with (Finite.powerset with pairs), inside127  have inside : kuhnSimplices(p, n) ⊆ 𝒫(functionSpace(n, succ(p)))128    intros s hs129    have parts := kuhnSimplices.membership.forward with hs130    exact parts.left131  exact Finite.subset with (Finite.powerset with cube), inside132