Numerical recipes prescribe the concrete gradients on witness atoms
Lax342547.ConcreteRecipes · concepts/Lax342547/ConcreteRecipes.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
The bit prescriptions are chosen using only tags, tester summaries, and opposite role/p bits. They work for every later choice of actual atoms and mixers realizing that data and those distinct-atom evaluations. This is the deterministic prescription assertion of Lemma 6.2(iii), without an assumption of independence or occurrence of fixed-point evaluations.
Concept map
Lean source view on GitHub
| 1 | import Lax342547.AtomProducts |
| 2 | import Lax342547.RecipeRows |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Numerical recipes prescribe the concrete gradients on witness atoms |
| 7 | type: lemma |
| 8 | --- |
| 9 | The bit prescriptions are chosen using only tags, tester summaries, and |
| 10 | opposite role/p bits. They work for every later choice of actual atoms and |
| 11 | mixers realizing that data and those distinct-atom evaluations. This is |
| 12 | the deterministic prescription assertion of Lemma 6.2(iii), without an |
| 13 | assumption of independence or occurrence of fixed-point evaluations. |
| 14 | -/ |
| 15 | |
| 16 | namespace Lax342547.ConcreteRecipes |
| 17 | |
| 18 | open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry |
| 19 | open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.WitnessAtoms |
| 20 | |
| 21 | def RecipeGradients {I J : Type} [Fintype I] [Fintype J] |
| 22 | {k n b degree r copies : ℕ} {hr : 2 * r ≤ n} |
| 23 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 24 | (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 25 | (atoms : I ⊕ J → PointAtom k n b degree) (p : I ⊕ J → Binary) : Prop := |
| 26 | (∀ i : I, D.role (atoms (.inl i)).profile + |
| 27 | gradient D L R (∑ t : I, (atoms (.inl t)).profile) (atoms (.inl i)).profile = 0) ∧ |
| 28 | (∀ j : J, D.role (atoms (.inr j)).profile + |
| 29 | gradient D L R (∑ t : I, (atoms (.inl t)).profile) (atoms (.inr j)).profile = p (.inr j)) ∧ |
| 30 | (∀ j : J, D.role (atoms (.inr j)).profile + |
| 31 | gradient D L R (∑ t : J, (atoms (.inr t)).profile) (atoms (.inr j)).profile = 0) ∧ |
| 32 | (∀ i : I, D.role (atoms (.inl i)).profile + |
| 33 | gradient D L R (∑ t : J, (atoms (.inr t)).profile) (atoms (.inl i)).profile = p (.inl i)) |
| 34 | |
| 35 | axiom prescribe {I J : Type} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] |
| 36 | {k copies : ℕ} (hk : 0 < k) (hcopies : 0 < copies) |
| 37 | (data : I ⊕ J → Numerical k) (opposite p : I ⊕ J → Binary) |
| 38 | (hrole₁ : (∑ i : I, (data (Sum.inl i)).role) + (∑ i : I, opposite (Sum.inl i)) = 1) |
| 39 | (hrole₂ : (∑ j : J, (data (Sum.inr j)).role) + (∑ j : J, opposite (Sum.inr j)) = 1) |
| 40 | (hcoupled : (∑ i : I, (p (Sum.inl i) + opposite (Sum.inl i))) = |
| 41 | ∑ j : J, (p (Sum.inr j) + opposite (Sum.inr j))) : |
| 42 | ∃ lbits rbits : (I ⊕ J) → (I ⊕ J) → ProductIndex k copies → Binary, |
| 43 | (∀ x y t, ¬ allowedIndex (data x) (data y) t → lbits x y t = 0 ∧ rbits x y t = 0) ∧ |
| 44 | ∀ (n b degree r : ℕ) (hr : 2 * r ≤ n) |
| 45 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 46 | (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 47 | (atoms : I ⊕ J → PointAtom k n b degree), |
| 48 | (∀ x, (atoms x).numerical hr = data x) → |
| 49 | (∀ x y, x ≠ y → ∀ t, allowedIndex (data x) (data y) t → |
| 50 | (L t.1 t.2.1 t.2.2).toBilin' (atoms x).vector (atoms y).vector = lbits x y t ∧ |
| 51 | (R t.1 t.2.1 t.2.2).toBilin' (atoms x).vector (atoms y).vector = rbits x y t) → |
| 52 | RecipeGradients D L R atoms p |
| 53 | |
| 54 | end Lax342547.ConcreteRecipes |
| 55 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments