The symmetric binary gradient form

Lax342547.GradientForm · concepts/Lax342547/GradientForm.lean · lax-342547

proven

Loading review…

The form in (2.8)–(2.10): $a\otimes a$ , the symmetric tester terms, and the symmetrization of the mixer form. Its diagonal is $a$ .

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

Show types on hover

1	import Lax342547.HoleRelation
2	import Lax342547.MomentSpace
3
4	/-!
5	---
6	title: The symmetric binary gradient form
7	type: lemma
8	---
9	The form in (2.8)–(2.10): $a\otimes a$ , the symmetric tester terms,
10	and the symmetrization of the mixer form. Its diagonal is $a$ .
11	-/
12
13	namespace Lax342547.GradientForm
14
15	open Lax342547.MomentSpace
16
17	variable {X Tag : Type} [AddCommGroup X] [Module Binary X] [Fintype Tag]
18
19	def rankOne (a b : X →ₗ[Binary] Binary) : LinearMap.BilinForm Binary X := a.smulRight b
20
21	def form (a : X →ₗ[Binary] Binary) (aTag bTag : Tag → X →ₗ[Binary] Binary)
22	(B : LinearMap.BilinForm Binary X) : LinearMap.BilinForm Binary X :=
23	rankOne a a + (∑ t, (rankOne (aTag t) (bTag t) + rankOne (bTag t) (aTag t))) + B + B.flip
24
25	axiom form_properties (a : X →ₗ[Binary] Binary) (aTag bTag : Tag → X →ₗ[Binary] Binary)
26	(B : LinearMap.BilinForm Binary X) :
27	(∀ x y, form a aTag bTag B x y = form a aTag bTag B y x) ∧
28	∀ x, form a aTag bTag B x x = a x
29
30	end Lax342547.GradientForm
31

Builds on

Used by

From Mathlib

none

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive