Mathlib.Combinatorics.JohnsonKneser
Johnson harmonic decomposition of uniform subset slices and the Kneser disjointness operator's degree-wise eigenvalues.
Basic 9 core · 7 supporting This module defines the uniform M-slice of Fin n, real functions on that slice, the uniform inner product and mean, inclusion monomials, and the nested subspaces spanned by monomials of bounded degree. ★ degreeAtMost_eq_top
Uniform slices and their inclusion-degree filtration
This module defines the uniform M-slice of Fin n, real functions on that
slice, the uniform inner product and mean, inclusion monomials, and the nested
subspaces spanned by monomials of bounded degree. It contains no
Johnson/Kneser spectral conclusions.
def Omega reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population with n labelled units and a requested subset size M, the uniform slice is represented by the M-element subsets of that population.
Definition (Lean source)
parameters
n M :
ℕ
def
Omega n M :
Type
given by
abbrev SliceFn reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population size n and a slice size M, the slice-function space is the real Euclidean space of functions on that uniform slice.
Definition (Lean source)
def sliceInner reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a first slice function and a second slice function, the uniform-slice inner product is the average of their pointwise products over all slice points.
def mean reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a slice function, its uniform mean is the average of its values over the slice.
def constFn reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a real value, the constant slice function is the function taking that value at every slice point.
def center reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a slice function, its centered version is obtained by subtracting its uniform mean at every slice point.
def inclusionMonomial reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a set of labelled units, its inclusion monomial is one on slice points containing that set and zero elsewhere.
def degreeAtMost reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population size, a slice size, and a degree bound, the degree-at-most subspace is the linear span of inclusion monomials indexed by sets no larger than that bound.
theorem degreeAtMost_eq_top reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
When the requested slice size is feasible, inclusion monomials through degree M span every real function on the uniform slice.
Formal statement
Proof (Lean source)
theorem degreeAtMost_eq_top (hMn : M ≤ n) :
degreeAtMost n M M = ⊤ := by
apply top_unique
intro f hf
have hsubset_iff (A B : Omega n M) : A.1 ⊆ B.1 ↔ A = B := by
constructor
· intro hAB
apply Subtype.ext
exact Finset.eq_of_subset_of_card_le hAB (by rw [A.2, B.2])
· rintro rfl
exact Finset.Subset.rfl
have hmono (A : Omega n M) :
inclusionMonomial (M := M) A.1 ∈ degreeAtMost n M M :=
Submodule.subset_span ⟨A.1, A.2.le, rfl⟩
have hsum :
(∑ A : Omega n M, f A • inclusionMonomial (M := M) A.1) ∈
degreeAtMost n M M :=
Submodule.sum_mem _ fun A _ => Submodule.smul_mem _ _ (hmono A)
convert hsum using 1
ext B
simp [inclusionMonomial, hsubset_iff]
7 supporting declarations (lemmas, instances)
-
instDecidableEqOmegainstancederiving Fintype, DecidableEq -
instFintypeOmegainstancederiving Fintype, DecidableEq -
degreeAtMost_monotheorem — When the first degree bound does not exceed the second, every function in the first inclusion-degree subspace also belongs to the second.hypothesesn :sharedℕM :sharedℕd e :ℕhde :d ≤ econclusiondegreeAtMost n M d ≤ degreeAtMost n M eProof (Lean source)
theorem degreeAtMost_mono {d e : ℕ} (hde : d ≤ e) : degreeAtMost n M d ≤ degreeAtMost n M e := by exact Submodule.span_mono fun f ⟨S, hSd, hf⟩ => ⟨S, hSd.trans hde, hf⟩ -
mem_degreeAtMost_zero_ifftheorem — When the requested slice size is feasible, a slice function belongs to the degree-zero subspace exactly when it is constant, for the given slice function.hypothesesconclusionf ∈ degreeAtMost n M 0 ↔ ∃ c : ℝ, f = constFn cProof (Lean source)
theorem mem_degreeAtMost_zero_iff (hMn : M ≤ n) (f : SliceFn n M) : f ∈ degreeAtMost n M 0 ↔ ∃ c : ℝ, f = constFn c := by have hgen : {g : SliceFn n M | ∃ S : Finset (Fin n), S.card ≤ 0 ∧ g = inclusionMonomial (M := M) S} = {constFn 1} := by ext g simp only [Set.mem_ofPred_eq, Set.mem_singleton_iff] constructor · rintro ⟨S, hS, rfl⟩ have hS0 : S = ∅ := Finset.card_eq_zero.mp (Nat.eq_zero_of_le_zero hS) subst S ext A simp [inclusionMonomial, constFn] · intro hg subst g refine ⟨∅, by simp, ?_⟩ ext A simp [inclusionMonomial, constFn] rw [degreeAtMost, hgen, Submodule.mem_span_singleton] constructor · rintro ⟨c, hc⟩ refine ⟨c, hc.symm.trans ?_⟩ ext A simp [constFn] · rintro ⟨c, rfl⟩ refine ⟨c, ?_⟩ ext A simp [constFn] -
card_omegatheorem — When the requested slice size is feasible, the uniform slice has exactly the usual binomial number of points.Proof (Lean source)
theorem card_omega (hMn : M ≤ n) : card (Omega n M) = n.choose M := by let e : Omega n M ≃ {S // S ∈ (Finset.univ : Finset (Fin n)).powersetCard M} := { toFun := fun A => ⟨A.1, by simp [A.2]⟩ invFun := fun S => ⟨S.1, (Finset.mem_powersetCard.mp S.2).2⟩ left_inv := fun A => by cases A; rfl right_inv := fun S => by cases S; rfl } calc card (Omega n M) = card {S // S ∈ (Finset.univ : Finset (Fin n)).powersetCard M} := Fintype.card_congr e _ = ((Finset.univ : Finset (Fin n)).powersetCard M).card := Fintype.card_coe _ _ = n.choose M := by simp -
sliceInner_eqtheorem — When the requested slice size is feasible, the uniform inner product of the two given slice functions equals the ordinary function-space inner product divided by the number of slice points, for the first function and the second function.hypothesesconclusionsliceInner f g = (n.choose M : ℝ)⁻¹ * inner ℝ f gProof (Lean source)
theorem sliceInner_eq (hMn : M ≤ n) (f g : SliceFn n M) : sliceInner f g = (n.choose M : ℝ)⁻¹ * inner ℝ f g := by rw [sliceInner, card_omega hMn, PiLp.inner_apply] simp only [Real.inner_apply] -
mean_constFntheorem — When the requested slice size is feasible, the uniform mean of the given constant slice function equals its constant value, for the real value.hypothesesM :sharedℕn :sharedℕhMn :M ≤ nc :ℝconclusionmean (constFn (n := n) (M := M) c) = cProof (Lean source)
theorem mean_constFn (hMn : M ≤ n) (c : ℝ) : mean (constFn (n := n) (M := M) c) = c := by have hchoose : n.choose M ≠ 0 := Nat.ne_of_gt (Nat.choose_pos hMn) simp [mean, constFn, card_omega hMn, hchoose]
Harmonics 3 core · 12 supporting The degree-k Johnson harmonic subspace is the new orthogonal layer in the inclusion-degree filtration. ★ sum_positive_harmonicProjection_eq_center
Canonical Johnson harmonic subspaces and projections
The degree-k Johnson harmonic subspace is the new orthogonal layer in the
inclusion-degree filtration. Finite-dimensional orthogonal projection gives a
canonical linear projector. The declarations here state its range,
fixed-point, residual-orthogonality, cross-degree orthogonality, and complete
slice decomposition properties.
def johnsonHarmonic reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population size and a slice size, the Johnson harmonic subspaces are the degree-zero inclusion layer at degree zero and the new orthogonal inclusion-degree layer at each positive degree.
Definition (Lean source)
parameters
n M :
ℕ
given by
clause 1
| 0 => degreeAtMost n M 0
clause 2
| d + 1 => degreeAtMost n M (d + 1) ⊓ (degreeAtMost n M d)ᗮ
def harmonicProjection reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population size, a slice size, and a harmonic degree, the harmonic projection is the canonical linear orthogonal projection onto that degree's Johnson harmonic subspace.
Definition (Lean source)
theorem sum_positive_harmonicProjection_eq_center reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
When the requested slice size is feasible, centering the given slice function equals the sum of its positive-degree harmonic projections, for the slice function.
Formal statement
hypotheses
conclusion
(∑ k ∈ Finset.univ.filter (fun k : Fin (M + 1) => 0 < k.1), harmonicProjection n M k f)
= center f
Proof (Lean source)
theorem sum_positive_harmonicProjection_eq_center (hMn : M ≤ n)
(f : SliceFn n M) :
(∑ k ∈ Finset.univ.filter (fun k : Fin (M + 1) => 0 < k.1),
harmonicProjection n M k f) = center f := by
let z : Fin (M + 1) := ⟨0, Nat.zero_lt_succ M⟩
have hnot :
Finset.univ.filter (fun k : Fin (M + 1) => ¬ 0 < k.1) = {z} := by
ext k
simp only [mem_filter, Finset.mem_univ, true_and,
mem_singleton]
constructor
· intro hk
apply Fin.ext
simp only [z]
omega
· rintro rfl
simp [z]
have hsplit := Finset.sum_filter_add_sum_filter_not
(Finset.univ : Finset (Fin (M + 1)))
(fun k : Fin (M + 1) => 0 < k.1)
(fun k => harmonicProjection n M k f)
rw [hnot, Finset.sum_singleton, sum_harmonicProjection_eq hMn f,
harmonicProjection_zero_eq_mean hMn f] at hsplit
rw [center]
exact eq_sub_of_add_eq hsplit
12 supporting declarations (lemmas, instances)
-
harmonicProjection_addtheorem — For a harmonic degree, the projection of the sum equals the sum of the projections of the first slice function and the second slice function.hypothesesconclusionProof (Lean source)
theorem harmonicProjection_add (k : Fin (M + 1)) (f g : SliceFn n M) : harmonicProjection n M k (f + g) = harmonicProjection n M k f + harmonicProjection n M k g := map_add (harmonicProjection n M k) f g -
harmonicProjection_smultheorem — For a harmonic degree, a real scalar, and a slice function, projecting after scalar multiplication equals scalar multiplication after projection.hypothesesconclusionharmonicProjection n M k (c • f) = c • harmonicProjection n M k fProof (Lean source)
theorem harmonicProjection_smul (k : Fin (M + 1)) (c : ℝ) (f : SliceFn n M) : harmonicProjection n M k (c • f) = c • harmonicProjection n M k f := map_smul (harmonicProjection n M k) c f -
degreeAtMost_succ_eq_sup_harmonictheorem — For a degree bound, the next inclusion-degree space is the sum of the preceding space and its new Johnson harmonic layer.hypothesesn :sharedℕM :sharedℕd :ℕconclusionProof (Lean source)
theorem degreeAtMost_succ_eq_sup_harmonic (d : ℕ) : degreeAtMost n M (d + 1) = degreeAtMost n M d ⊔ johnsonHarmonic n M (d + 1) := by rw [johnsonHarmonic, inf_comm] exact (Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection (degreeAtMost_mono (Nat.le_succ d))).symm -
degreeAtMost_eq_iSup_harmonictheorem — The full degree-at-most-M space is the supremum of the Johnson harmonic layers from degree zero through degree M.hypothesesn :sharedℕM :sharedℕconclusionProof (Lean source)
theorem degreeAtMost_eq_iSup_harmonic : degreeAtMost n M M = ⨆ k : Fin (M + 1), johnsonHarmonic n M k.1 := by exact degreeAtMost_eq_iSup_harmonic_fin M -
harmonicProjection_memtheorem — For a harmonic degree and a slice function, the projected component belongs to that degree's Johnson harmonic subspace.hypothesesconclusionharmonicProjection n M k f ∈ johnsonHarmonic n M k.1Proof (Lean source)
theorem harmonicProjection_mem (k : Fin (M + 1)) (f : SliceFn n M) : harmonicProjection n M k f ∈ johnsonHarmonic n M k.1 := by exact Submodule.starProjection_apply_mem _ _ -
harmonicProjection_eq_self_ifftheorem — For a harmonic degree and a slice function, projection leaves the function unchanged exactly when it already lies in that harmonic subspace.hypothesesconclusionharmonicProjection n M k f = f ↔ f ∈ johnsonHarmonic n M k.1Proof (Lean source)
theorem harmonicProjection_eq_self_iff (k : Fin (M + 1)) (f : SliceFn n M) : harmonicProjection n M k f = f ↔ f ∈ johnsonHarmonic n M k.1 := by exact Submodule.starProjection_eq_self_iff -
harmonicProjection_idemtheorem — For a harmonic degree and a slice function, applying the harmonic projection twice gives the same component as applying it once.hypothesesconclusionProof (Lean source)
theorem harmonicProjection_idem (k : Fin (M + 1)) (f : SliceFn n M) : harmonicProjection n M k (harmonicProjection n M k f) = harmonicProjection n M k f := by exact Submodule.starProjection_eq_self_iff.mpr (Submodule.starProjection_apply_mem _ _) -
sliceInner_residual_eq_zerotheorem — When the requested slice size is feasible, the residual after projection is orthogonal under the uniform slice inner product to the given harmonic function, for a harmonic degree, a slice function, a comparison function, and evidence that the comparison function is in that harmonic subspace.hypothesesM :sharedℕn :sharedℕhMn :M ≤ nk :Fin (M + 1)f g :SliceFn n Mhg :g ∈ johnsonHarmonic n M k.1conclusionsliceInner (f - harmonicProjection n M k f) g = 0Proof (Lean source)
theorem sliceInner_residual_eq_zero (hMn : M ≤ n) (k : Fin (M + 1)) (f g : SliceFn n M) (hg : g ∈ johnsonHarmonic n M k.1) : sliceInner (f - harmonicProjection n M k f) g = 0 := by rw [sliceInner_eq hMn] change (n.choose M : ℝ)⁻¹ * inner ℝ (f - (johnsonHarmonic n M k.1).starProjection f) g = 0 rw [Submodule.starProjection_inner_eq_zero _ _ hg, mul_zero] -
johnsonHarmonic_pairwise_orthogonaltheorem — When the requested slice size is feasible and the two harmonic degrees are distinct, functions in those two Johnson harmonic subspaces are orthogonal under the uniform slice inner product, for the first function's membership evidence and the second function's membership evidence.hypothesesM :sharedℕn :sharedℕhMn :M ≤ nj k :Fin (M + 1)hjk :j ≠ kf g :SliceFn n Mhf :f ∈ johnsonHarmonic n M j.1hg :g ∈ johnsonHarmonic n M k.1conclusionsliceInner f g = 0Proof (Lean source)
theorem johnsonHarmonic_pairwise_orthogonal (hMn : M ≤ n) {j k : Fin (M + 1)} (hjk : j ≠ k) {f g : SliceFn n M} (hf : f ∈ johnsonHarmonic n M j.1) (hg : g ∈ johnsonHarmonic n M k.1) : sliceInner f g = 0 := by rw [sliceInner_eq hMn, johnsonHarmonic_inner_eq_zero hjk hf hg, mul_zero] -
sum_harmonicProjection_eqtheorem — When the requested slice size is feasible, the given slice function equals the finite sum of its harmonic projections from degree zero through degree M, for the slice function.hypothesesconclusion(∑ k : Fin (M + 1), harmonicProjection n M k f) = fProof (Lean source)
theorem sum_harmonicProjection_eq (hMn : M ≤ n) (f : SliceFn n M) : (∑ k : Fin (M + 1), harmonicProjection n M k f) = f := by let V : Fin (M + 1) → Submodule ℝ (SliceFn n M) := fun k => johnsonHarmonic n M k.1 have hV : OrthogonalFamily ℝ (fun k => V k) fun k => (V k).subtypeₗᵢ := by intro j k hjk x y exact johnsonHarmonic_inner_eq_zero hjk x.2 y.2 have htop : iSup V = ⊤ := by rw [← degreeAtMost_eq_iSup_harmonic, degreeAtMost_eq_top hMn] exact hV.sum_projection_of_mem_iSup f (by rw [htop]; trivial) -
harmonicProjection_zero_eq_meantheorem — When the requested slice size is feasible, the degree-zero projection of the given slice function is the constant function at its uniform mean, for the slice function.hypothesesconclusionProof (Lean source)
theorem harmonicProjection_zero_eq_mean (hMn : M ≤ n) (f : SliceFn n M) : harmonicProjection n M (⟨0, Nat.zero_lt_succ M⟩ : Fin (M + 1)) f = constFn (mean f) := by change (degreeAtMost n M 0).starProjection f = constFn (mean f) apply Submodule.eq_starProjection_of_mem_of_inner_eq_zero · exact (mem_degreeAtMost_zero_iff hMn _).2 ⟨mean f, rfl⟩ · intro g hg obtain ⟨c, rfl⟩ := (mem_degreeAtMost_zero_iff hMn g).1 hg rw [PiLp.inner_apply] simp only [Real.inner_apply, PiLp.sub_apply, constFn] rw [← Finset.sum_mul] simp only [Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul] rw [mean, card_omega hMn] rw [show (Finset.univ : Finset (Omega n M)).card = n.choose M by simpa using card_omega hMn] have hcard : (n.choose M : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.ne_of_gt (Nat.choose_pos hMn)) field_simp ring -
harmonicProjection_pairwise_orthogonaltheorem — When the requested slice size is feasible and the two harmonic degrees are distinct, the corresponding projected components of the given function are orthogonal under the uniform slice inner product, for the slice function.hypothesesconclusionProof (Lean source)
theorem harmonicProjection_pairwise_orthogonal (hMn : M ≤ n) (f : SliceFn n M) {j k : Fin (M + 1)} (hjk : j ≠ k) : sliceInner (harmonicProjection n M j f) (harmonicProjection n M k f) = 0 := by exact johnsonHarmonic_pairwise_orthogonal hMn hjk (harmonicProjection_mem j f) (harmonicProjection_mem k f)
Kneser 4 core · 10 supporting This module defines the unnormalized adjacency sum over disjoint slice points. ★ kneserAdjacency_eigen
The Kneser disjointness operator on Johnson harmonics
This module defines the unnormalized adjacency sum over disjoint slice points. It states the classical Kneser eigenvalue on every canonical Johnson harmonic degree, as well as the normalized falling-factorial form.
def kneserAdjacency reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population size and a slice size, the unnormalized Kneser adjacency operator is specified by summing a function over all equally sized subsets disjoint from the argument, preserving addition, and commuting with real scalar multiplication.
Definition (Lean source)
parameters
n M :
ℕ
given by
clause 1
clause 2
clause 3
map_smul' c f := by ext A simp [Finset.mul_sum]
def disjointIndicator reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a set of labelled units, its disjointness indicator is one at slice points disjoint from that set and zero elsewhere.
theorem kneserAdjacency_eigen reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
When two disjoint slice-sized subsets can fit in the population, the selected harmonic degree, and the given function belongs to that degree's Johnson harmonic subspace, unnormalized Kneser adjacency acts by its classical signed binomial eigenvalue, for the slice function.
Formal statement
hypotheses
M :
ℕ
n :
ℕ
h2 :
2 * M ≤ n
k :
Fin (M + 1)
f :
SliceFn n M
hf :
f ∈ johnsonHarmonic n M k.1
conclusion
kneserAdjacency n M f = (((-1 : ℝ) ^ k.1) * ((n - M - k.1).choose (M - k.1) : ℝ)) • f
Proof (Lean source)
theorem kneserAdjacency_eigen (h2 : 2 * M ≤ n) (k : Fin (M + 1))
(f : SliceFn n M) (hf : f ∈ johnsonHarmonic n M k.1) :
kneserAdjacency n M f =
(((-1 : ℝ) ^ k.1) * ((n - M - k.1).choose (M - k.1) : ℝ)) • f := by
have hMn : M ≤ n := by omega
cases hk : k.1 with
| zero =>
have hf0 : f ∈ degreeAtMost n M 0 := by
simpa [johnsonHarmonic, hk] using hf
obtain ⟨c, rfl⟩ := (mem_degreeAtMost_zero_iff hMn _).1 hf0
have hconst :
constFn (n := n) (M := M) c =
c • inclusionMonomial (M := M) (∅ : Finset (Fin n)) := by
ext A
simp [constFn, inclusionMonomial]
rw [hconst, map_smul,
kneserAdjacency_inclusionMonomial_eq h2 ∅ (by simp)]
ext A
simp [disjointIndicator, inclusionMonomial, mul_comm]
| succ d =>
have hdM : d + 1 ≤ M := by omega
have hfharm :
f ∈ degreeAtMost n M (d + 1) ⊓ (degreeAtMost n M d)ᗮ := by
simpa [johnsonHarmonic, hk] using hf
have hf' : f ∈ degreeAtMost n M (d + 1) := by
exact hfharm.1
let eig : ℝ :=
((-1 : ℝ) ^ (d + 1)) * ((n - M - (d + 1)).choose (M - (d + 1)) : ℝ)
let r : SliceFn n M := kneserAdjacency n M f - eig • f
have hr : r ∈ degreeAtMost n M d := by
have h := kneserAdjacency_sub_eigen_mem_lower h2 (d := d + 1)
(by omega) hdM f hf'
simpa [r, eig] using h
have hforth : ∀ g ∈ degreeAtMost n M d, sliceInner f g = 0 := by
intro g hg
rw [sliceInner_eq hMn, real_inner_comm]
have hfg : inner ℝ g f = 0 := by
exact hfharm.2 g hg
rw [hfg, mul_zero]
have hrorth : ∀ g ∈ degreeAtMost n M d, sliceInner r g = 0 := by
intro g hg
have hAg : kneserAdjacency n M g ∈ degreeAtMost n M d :=
kneserAdjacency_mem_degreeAtMost h2 (by omega) g hg
have hexpand :
sliceInner r g = sliceInner (kneserAdjacency n M f) g -
eig * sliceInner f g := by
rw [sliceInner_eq hMn, sliceInner_eq hMn, sliceInner_eq hMn]
simp only [r, inner_sub_left, inner_smul_left]
change (n.choose M : ℝ)⁻¹ *
(inner ℝ (kneserAdjacency n M f) g - eig * inner ℝ f g) =
(n.choose M : ℝ)⁻¹ * inner ℝ (kneserAdjacency n M f) g -
eig * ((n.choose M : ℝ)⁻¹ * inner ℝ f g)
ring
have hself := sliceInner_kneserAdjacency (n := n) (M := M) f g
rw [hexpand, hself, hforth g hg,
hforth (kneserAdjacency n M g) hAg]
ring
have hs : sliceInner r r = 0 := hrorth r hr
have hchoose : n.choose M ≠ 0 := Nat.ne_of_gt (Nat.choose_pos hMn)
have hscale : ((n.choose M : ℝ)⁻¹) ≠ 0 :=
inv_ne_zero (Nat.cast_ne_zero.mpr hchoose)
have hir : inner ℝ r r = 0 := by
rw [sliceInner_eq hMn] at hs
exact (mul_eq_zero.mp hs).resolve_left hscale
have hr0 : r = 0 := inner_self_eq_zero.mp hir
exact sub_eq_zero.mp (by simpa [r, eig, hk] using hr0)
def normalizedKneserAdjacency reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.JohnsonKneser
For a population size and a slice size, the normalized Kneser adjacency operator is the unnormalized disjointness sum divided by the number of disjoint neighbors.
Definition (Lean source)
10 supporting declarations (lemmas, instances)
-
disjointIndicator_eq_sum_powersettheorem — For a set of labelled units, its disjointness indicator equals the alternating inclusion-exclusion sum of the inclusion monomials of its subsets.hypothesesconclusiondisjointIndicator (M := M) S= ∑ T ∈ S.powerset, ((-1 : ℝ) ^ T.card) • inclusionMonomial (M := M) TProof (Lean source)
theorem disjointIndicator_eq_sum_powerset (S : Finset (Fin n)) : disjointIndicator (M := M) S = ∑ T ∈ S.powerset, ((-1 : ℝ) ^ T.card) • inclusionMonomial (M := M) T := by ext A simp only [disjointIndicator, inclusionMonomial] simp have hsum : (∑ T ∈ (S ∩ A.1).powerset, (-1 : ℝ) ^ T.card) = if S ∩ A.1 = ∅ then 1 else 0 := by exact_mod_cast (Finset.sum_powerset_neg_one_pow_card (x := S ∩ A.1)) have hfilter : S.powerset.filter (fun T => T ⊆ A.1) = (S ∩ A.1).powerset := by ext T simp only [mem_filter, Finset.mem_powerset] constructor · rintro ⟨hTS, hTA⟩ x hx exact Finset.mem_inter.mpr ⟨hTS hx, hTA hx⟩ · intro hT exact ⟨hT.trans Finset.inter_subset_left, hT.trans Finset.inter_subset_right⟩ calc (if Disjoint S A.1 then 1 else 0) = if S ∩ A.1 = ∅ then 1 else 0 := by simp only [Finset.disjoint_iff_inter_eq_empty] _ = ∑ T ∈ (S ∩ A.1).powerset, (-1 : ℝ) ^ T.card := hsum.symm _ = ∑ T ∈ S.powerset.filter (fun T => T ⊆ A.1), (-1 : ℝ) ^ T.card := by rw [hfilter] _ = ∑ T ∈ S.powerset, if T ⊆ A.1 then (-1 : ℝ) ^ T.card else 0 := by rw [Finset.sum_filter] -
kneserAdjacency_inclusionMonomial_eqtheorem — When two disjoint slice-sized subsets can fit in the population and the indexing set is no larger than the slice size, Kneser adjacency maps the given inclusion monomial to its disjointness indicator times the number of compatible completions, for the indexing set.hypothesesconclusionkneserAdjacency n M (inclusionMonomial (M := M) S)= ((n - M - S.card).choose (M - S.card) : ℝ) • disjointIndicator (M := M) SProof (Lean source)
theorem kneserAdjacency_inclusionMonomial_eq (h2 : 2 * M ≤ n) (S : Finset (Fin n)) (hSM : S.card ≤ M) : kneserAdjacency n M (inclusionMonomial (M := M) S) = ((n - M - S.card).choose (M - S.card) : ℝ) • disjointIndicator (M := M) S := by ext A simp [kneserAdjacency, inclusionMonomial, disjointIndicator] by_cases hSA : Disjoint S A.1 · rw [if_pos hSA] let U : Finset (Fin n) := univ \ A.1 let goodOmega : Finset (Omega n M) := Finset.univ.filter (fun B => Disjoint A.1 B.1 ∧ S ⊆ B.1) let goodSets : Finset (Finset (Fin n)) := (U.powersetCard M).filter (fun B => S ⊆ B) have hSsubU : S ⊆ U := by intro x hxS exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ x, fun hxA => Finset.disjoint_left.mp hSA hxS hxA⟩ have hcardU : U.card = n - M := by simp only [U] rw [Finset.card_sdiff_of_subset (Finset.subset_univ A.1), A.2] simp have hcard : goodOmega.card = goodSets.card := by apply Finset.card_bij (fun B _ => B.1) · intro B hB simp only [goodOmega, mem_filter, Finset.mem_univ, true_and] at hB simp only [goodSets, mem_filter, Finset.mem_powersetCard] refine ⟨⟨?_, B.2⟩, hB.2⟩ intro x hxB exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ x, fun hxA => Finset.disjoint_left.mp hB.1 hxA hxB⟩ · intro B₁ hB₁ B₂ hB₂ h exact Subtype.ext h · intro C hC simp only [goodSets, mem_filter, Finset.mem_powersetCard] at hC let B : Omega n M := ⟨C, hC.1.2⟩ have hAB : Disjoint A.1 C := by rw [Finset.disjoint_left] intro x hxA hxC exact (Finset.mem_sdiff.mp (hC.1.1 hxC)).2 hxA refine ⟨B, ?_, rfl⟩ change B ∈ goodOmega rw [mem_filter] exact ⟨Finset.mem_univ B, hAB, hC.2⟩ have hgoodSets : goodSets.card = (n - M - S.card).choose (M - S.card) := by rw [show goodSets = (U.powersetCard M).filter (fun B => S ⊆ B) by rfl, Finset.card_filter_powersetCard_subset S U M hSsubU hSM, hcardU] calc (∑ B : Omega n M, if Disjoint A.1 B.1 then if S ⊆ B.1 then 1 else 0 else 0) = (goodOmega.card : ℝ) := by simp only [goodOmega, Finset.card_filter, Nat.cast_sum, Nat.cast_ite, cast_one, cast_zero] apply Finset.sum_congr rfl intro B _ by_cases hAB : Disjoint A.1 B.1 <;> by_cases hSB : S ⊆ B.1 <;> simp [hAB, hSB] _ = (goodSets.card : ℝ) := by rw [hcard] _ = ((n - M - S.card).choose (M - S.card) : ℝ) := by rw [hgoodSets] · rw [if_neg hSA] apply Finset.sum_eq_zero intro B _ by_cases hAB : Disjoint A.1 B.1 · rw [if_pos hAB, if_neg] intro hSB apply hSA rw [Finset.disjoint_left] intro x hxS hxA exact Finset.disjoint_left.mp hAB hxA (hSB hxS) · rw [if_neg hAB] -
kneserAdjacency_inclusionMonomial_mod_lowertheorem — When two disjoint slice-sized subsets can fit in the population, the degree is positive, the indexing set has exactly that degree, and the degree does not exceed the slice size, Kneser adjacency differs from its classical degree eigenvalue times that monomial only by a lower-degree function.hypothesesM :sharedℕn :sharedℕh2 :2 * M ≤ nd :ℕhd :0 < dhSd :S.card = dhdM :d ≤ MconclusionkneserAdjacency n M (inclusionMonomial (M := M) S)- (((-1 : ℝ) ^ d) * ((n - M - d).choose (M - d) : ℝ)) • inclusionMonomial (M := M) S ∈ degreeAtMost n M (d - 1)Proof (Lean source)
theorem kneserAdjacency_inclusionMonomial_mod_lower (h2 : 2 * M ≤ n) {d : ℕ} (hd : 0 < d) (S : Finset (Fin n)) (hSd : S.card = d) (hdM : d ≤ M) : kneserAdjacency n M (inclusionMonomial (M := M) S) - (((-1 : ℝ) ^ d) * ((n - M - d).choose (M - d) : ℝ)) • inclusionMonomial (M := M) S ∈ degreeAtMost n M (d - 1) := by subst d have hSM : S.card ≤ M := hdM rw [kneserAdjacency_inclusionMonomial_eq h2 S hSM, disjointIndicator_eq_sum_powerset] let c : ℝ := ((n - M - S.card).choose (M - S.card) : ℝ) have hSps : S ∈ S.powerset := by simp have hlower : ∀ T ∈ S.powerset.erase S, inclusionMonomial (M := M) T ∈ degreeAtMost n M (S.card - 1) := by intro T hT have hTS : T ⊆ S := Finset.mem_powerset.mp (mem_of_mem_erase hT) have hTne : T ≠ S := Finset.ne_of_mem_erase hT have hcard : T.card ≤ S.card - 1 := by have : T.card < S.card := Finset.card_lt_card (Finset.ssubset_iff_subset_ne.mpr ⟨hTS, hTne⟩) omega exact Submodule.subset_span ⟨T, hcard, rfl⟩ have hsum : (∑ T ∈ S.powerset.erase S, (c * (-1 : ℝ) ^ T.card) • inclusionMonomial (M := M) T) ∈ degreeAtMost n M (S.card - 1) := by exact Submodule.sum_mem _ fun T hT => Submodule.smul_mem _ _ (hlower T hT) convert hsum using 1 rw [← Finset.sum_erase_add _ _ hSps] rw [smul_add, Finset.smul_sum] simp_rw [smul_smul] dsimp only [c] module -
kneserAdjacency_mem_degreeAtMosttheorem — When two disjoint slice-sized subsets can fit in the population, the degree bound does not exceed the slice size, and the given function belongs to that inclusion-degree subspace, Kneser adjacency remains in the same inclusion-degree subspace, for the slice function.hypothesesM :sharedℕn :sharedℕh2 :2 * M ≤ nd :ℕhdM :d ≤ Mf :SliceFn n Mhf :f ∈ degreeAtMost n M dconclusionkneserAdjacency n M f ∈ degreeAtMost n M dProof (Lean source)
theorem kneserAdjacency_mem_degreeAtMost (h2 : 2 * M ≤ n) {d : ℕ} (hdM : d ≤ M) (f : SliceFn n M) (hf : f ∈ degreeAtMost n M d) : kneserAdjacency n M f ∈ degreeAtMost n M d := by change f ∈ span ℝ {f | ∃ S : Finset (Fin n), S.card ≤ d ∧ f = inclusionMonomial (M := M) S} at hf refine Submodule.span_induction (p := fun f _ => kneserAdjacency n M f ∈ degreeAtMost n M d) ?_ ?_ ?_ ?_ hf · rintro _ ⟨S, hSd, rfl⟩ rw [kneserAdjacency_inclusionMonomial_eq h2 S (hSd.trans hdM), disjointIndicator_eq_sum_powerset] apply Submodule.smul_mem apply Submodule.sum_mem intro T hT apply Submodule.smul_mem exact Submodule.subset_span ⟨T, (Finset.card_le_card (Finset.mem_powerset.mp hT)).trans hSd, rfl⟩ · simpa using (degreeAtMost n M d).zero_mem · intro x y _ _ hx hy rw [map_add] exact (degreeAtMost n M d).add_mem hx hy · intro c x _ hx rw [map_smul] exact (degreeAtMost n M d).smul_mem c hx -
kneserAdjacency_sub_eigen_mem_lowertheorem — When two disjoint slice-sized subsets can fit in the population, the degree is positive, the degree does not exceed the slice size, and the given function has inclusion degree at most that degree, subtracting the classical degree eigenvalue leaves a function one degree lower, for the slice function.hypothesesM :sharedℕn :sharedℕh2 :2 * M ≤ nd :ℕhd :0 < dhdM :d ≤ Mf :SliceFn n Mhf :f ∈ degreeAtMost n M dconclusionkneserAdjacency n M f- (((-1 : ℝ) ^ d) * ((n - M - d).choose (M - d) : ℝ)) • f ∈ degreeAtMost n M (d - 1)Proof (Lean source)
theorem kneserAdjacency_sub_eigen_mem_lower (h2 : 2 * M ≤ n) {d : ℕ} (hd : 0 < d) (hdM : d ≤ M) (f : SliceFn n M) (hf : f ∈ degreeAtMost n M d) : kneserAdjacency n M f - (((-1 : ℝ) ^ d) * ((n - M - d).choose (M - d) : ℝ)) • f ∈ degreeAtMost n M (d - 1) := by let eig : ℝ := ((-1 : ℝ) ^ d) * ((n - M - d).choose (M - d) : ℝ) change f ∈ span ℝ {f | ∃ S : Finset (Fin n), S.card ≤ d ∧ f = inclusionMonomial (M := M) S} at hf change kneserAdjacency n M f - eig • f ∈ degreeAtMost n M (d - 1) refine Submodule.span_induction (p := fun f _ => kneserAdjacency n M f - eig • f ∈ degreeAtMost n M (d - 1)) ?_ ?_ ?_ ?_ hf · rintro _ ⟨S, hSd, rfl⟩ by_cases hcard : S.card = d · dsimp only [eig] exact kneserAdjacency_inclusionMonomial_mod_lower h2 hd S hcard hdM · have hSlo : S.card ≤ d - 1 := by omega have hmono : inclusionMonomial (M := M) S ∈ degreeAtMost n M (d - 1) := Submodule.subset_span ⟨S, hSlo, rfl⟩ exact (degreeAtMost n M (d - 1)).sub_mem (kneserAdjacency_mem_degreeAtMost h2 (by omega) _ hmono) ((degreeAtMost n M (d - 1)).smul_mem eig hmono) · simp · intro x y _ _ hx hy have hxy := (degreeAtMost n M (d - 1)).add_mem hx hy rw [map_add, smul_add] convert hxy using 1; module · intro c x _ hx have hcx := (degreeAtMost n M (d - 1)).smul_mem c hx rw [map_smul, smul_smul] convert hcx using 1; module -
sliceInner_kneserAdjacencytheorem — For a first slice function and a second slice function, Kneser adjacency is self-adjoint under the uniform slice inner product.hypothesesconclusionProof (Lean source)
theorem sliceInner_kneserAdjacency (f g : SliceFn n M) : sliceInner (kneserAdjacency n M f) g = sliceInner f (kneserAdjacency n M g) := by rw [sliceInner, sliceInner] congr 1 change (∑ A : Omega n M, (∑ B : Omega n M, if Disjoint A.1 B.1 then f B else 0) * g A) = ∑ A : Omega n M, f A * (∑ B : Omega n M, if Disjoint A.1 B.1 then g B else 0) simp_rw [Finset.sum_mul, Finset.mul_sum] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro A _ apply Finset.sum_congr rfl intro B _ by_cases hAB : Disjoint A.1 B.1 · rw [if_pos hAB, if_pos hAB.symm] · have hBA : ¬ Disjoint B.1 A.1 := fun h => hAB h.symm rw [if_neg hAB, if_neg hBA] simp -
kneserAdjacency_harmonicProjectiontheorem — When two disjoint slice-sized subsets can fit in the population, the selected harmonic degree, and the given slice function, Kneser adjacency acts on its projected harmonic component by the classical signed binomial eigenvalue.hypothesesconclusionkneserAdjacency n M (harmonicProjection n M k f)= (((-1 : ℝ) ^ k.1) * ((n - M - k.1).choose (M - k.1) : ℝ)) • harmonicProjection n M k fProof (Lean source)
theorem kneserAdjacency_harmonicProjection (h2 : 2 * M ≤ n) (k : Fin (M + 1)) (f : SliceFn n M) : kneserAdjacency n M (harmonicProjection n M k f) = (((-1 : ℝ) ^ k.1) * ((n - M - k.1).choose (M - k.1) : ℝ)) • harmonicProjection n M k f := by exact kneserAdjacency_eigen h2 k _ (harmonicProjection_mem k f) -
normalizedKneser_eigenvalue_eqtheorem — When two disjoint slice-sized subsets can fit in the population and the selected harmonic degree, the normalized Kneser eigenvalue magnitude equals the corresponding ratio of falling factorials.hypothesesconclusion((n - M).choose M : ℝ)⁻¹ * ((n - M - k.1).choose (M - k.1) : ℝ)= (M.descFactorial k.1 : ℝ) / ((n - M).descFactorial k.1 : ℝ)Proof (Lean source)
theorem normalizedKneser_eigenvalue_eq (h2 : 2 * M ≤ n) (k : Fin (M + 1)) : ((n - M).choose M : ℝ)⁻¹ * ((n - M - k.1).choose (M - k.1) : ℝ) = (M.descFactorial k.1 : ℝ) / ((n - M).descFactorial k.1 : ℝ) := by have hkM : k.1 ≤ M := by omega have hM : M ≤ n - M := by omega have hsub : M - k.1 ≤ n - M - k.1 := Nat.sub_le_sub_right hM k.1 have hdiff : n - M - k.1 - (M - k.1) = n - M - M := Nat.sub_sub_sub_cancel_right hkM rw [Nat.cast_choose ℝ hM, Nat.cast_choose ℝ hsub, hdiff] have hfacM : ((M - k.1).factorial : ℝ) * (M.descFactorial k.1 : ℝ) = (M.factorial : ℝ) := by exact_mod_cast Nat.factorial_mul_descFactorial hkM have hfacN : ((n - M - k.1).factorial : ℝ) * ((n - M).descFactorial k.1 : ℝ) = ((n - M).factorial : ℝ) := by exact_mod_cast Nat.factorial_mul_descFactorial (hkM.trans hM) have hdescN : ((n - M).descFactorial k.1 : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt (Nat.descFactorial_pos.mpr (hkM.trans hM))) field_simp [hdescN] rw [← hfacM, ← hfacN] ring -
normalizedKneserAdjacency_eigentheorem — When two disjoint slice-sized subsets can fit in the population, the selected harmonic degree, and the given function belongs to that degree's Johnson harmonic subspace, normalized Kneser adjacency acts by the signed falling-factorial eigenvalue, for the slice function.hypothesesM :sharedℕn :sharedℕh2 :2 * M ≤ nk :Fin (M + 1)f :SliceFn n Mhf :f ∈ johnsonHarmonic n M k.1conclusion= (((-1 : ℝ) ^ k.1) * ((M.descFactorial k.1 : ℝ) / ((n - M).descFactorial k.1 : ℝ))) • fProof (Lean source)
theorem normalizedKneserAdjacency_eigen (h2 : 2 * M ≤ n) (k : Fin (M + 1)) (f : SliceFn n M) (hf : f ∈ johnsonHarmonic n M k.1) : normalizedKneserAdjacency n M f = (((-1 : ℝ) ^ k.1) * ((M.descFactorial k.1 : ℝ) / ((n - M).descFactorial k.1 : ℝ))) • f := by rw [normalizedKneserAdjacency] simp only [LinearMap.smul_apply] rw [kneserAdjacency_eigen h2 k f hf, smul_smul] congr 1 rw [mul_left_comm ((n - M).choose M : ℝ)⁻¹] rw [normalizedKneser_eigenvalue_eq h2 k] -
normalizedKneserAdjacency_harmonicProjectiontheorem — When two disjoint slice-sized subsets can fit in the population, the selected harmonic degree, and the given slice function, normalized Kneser adjacency acts on its projected harmonic component by the signed falling-factorial eigenvalue.hypothesesconclusionnormalizedKneserAdjacency n M (harmonicProjection n M k f)= (((-1 : ℝ) ^ k.1) * ((M.descFactorial k.1 : ℝ) / ((n - M).descFactorial k.1 : ℝ))) • harmonicProjection n M k fProof (Lean source)
theorem normalizedKneserAdjacency_harmonicProjection (h2 : 2 * M ≤ n) (k : Fin (M + 1)) (f : SliceFn n M) : normalizedKneserAdjacency n M (harmonicProjection n M k f) = (((-1 : ℝ) ^ k.1) * ((M.descFactorial k.1 : ℝ) / ((n - M).descFactorial k.1 : ℝ))) • harmonicProjection n M k f := by exact normalizedKneserAdjacency_eigen h2 k _ (harmonicProjection_mem k f)