Quantitative comparison after cross-batch Gram conditioning
Lax342547.CrossBatchMixing · concepts/Lax342547/CrossBatchMixing.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
The actual cross-slot coefficient matrices give bit rank at least N for every nontrivial character. Separate bounded-density batch laws and bounded tests retain a uniform comparison after mutual Gram conditioning.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax342547.ConditionedMixing |
| 2 | import Lax342547.SlotWalsh |
| 3 | import Lax342547.RelativeEntropy |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Quantitative comparison after cross-batch Gram conditioning |
| 8 | type: lemma |
| 9 | --- |
| 10 | The actual cross-slot coefficient matrices give bit rank at least N for |
| 11 | every nontrivial character. Separate bounded-density batch laws and bounded |
| 12 | tests retain a uniform comparison after mutual Gram conditioning. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax342547.CrossBatchMixing |
| 16 | |
| 17 | open Lax342547.MomentSpace Lax342547.SlotWalsh Lax342547.FourierTests Lax342547.RelativeEntropy |
| 18 | |
| 19 | noncomputable def coefficient {I J S : Type} [Fintype S] |
| 20 | (C : S → Matrix I J Binary) (t : S → Binary) : Matrix I J Binary := ∑ s,t s • C s |
| 21 | |
| 22 | def crossBits {I J S : Type} [Fintype I] [Fintype J] (C : S → Matrix I J Binary) (N : ℕ) |
| 23 | (xy : ((Fin N × I → Binary) × (Fin N × J → Binary))) : S → Binary := |
| 24 | fun s => dotProduct xy.1 ((bitMatrix (C s) N).mulVec xy.2) |
| 25 | |
| 26 | axiom weighted_character_bound {I J S : Type} [Fintype I] [Fintype J] [Fintype S] |
| 27 | [DecidableEq I] [DecidableEq J] (C : S → Matrix I J Binary) (N : ℕ) |
| 28 | (α f : (Fin N × I → Binary) → ℝ) (β g : (Fin N × J → Binary) → ℝ) |
| 29 | (target t : S → Binary) (C₁ C₂ : ℝ) |
| 30 | (hα : ∀ x,0 ≤ α x ∧ α x ≤ C₁/(2 : ℝ)^(N*Fintype.card I)) |
| 31 | (hβ : ∀ y,0 ≤ β y ∧ β y ≤ C₂/(2 : ℝ)^(N*Fintype.card J)) |
| 32 | (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1) |
| 33 | (hC : coefficient C t ≠ 0) : |
| 34 | |characterMean (fun xy : (Fin N × I → Binary) × (Fin N × J → Binary) => |
| 35 | α xy.1*β xy.2*(f xy.1*g xy.2)) (crossBits C N) target t| ≤ |
| 36 | C₁*C₂/Real.sqrt ((2 : ℝ)^N) |
| 37 | |
| 38 | axiom cross_batch_comparison {I J S : Type} [Fintype I] [Fintype J] [Fintype S] |
| 39 | [DecidableEq I] [DecidableEq J] [DecidableEq S] (C : S → Matrix I J Binary) (N : ℕ) |
| 40 | (α f : (Fin N × I → Binary) → ℝ) (β g : (Fin N × J → Binary) → ℝ) |
| 41 | (target : S → Binary) (C₁ C₂ : ℝ) |
| 42 | (hα : Probability α) (hβ : Probability β) |
| 43 | (hcapA : ∀ x,α x ≤ C₁/(2 : ℝ)^(N*Fintype.card I)) |
| 44 | (hcapB : ∀ y,β y ≤ C₂/(2 : ℝ)^(N*Fintype.card J)) |
| 45 | (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1) |
| 46 | (hC : ∀ t : S → Binary,t ≠ 0 → coefficient C t ≠ 0) |
| 47 | (hsmall : C₁*C₂/Real.sqrt ((2 : ℝ)^N) ≤ 1/(2 : ℝ)^(Fintype.card S+1)) : |
| 48 | |patternMass (fun xy : (Fin N × I → Binary) × (Fin N × J → Binary) => |
| 49 | α xy.1*β xy.2*(f xy.1*g xy.2)) (crossBits C N) target/ |
| 50 | patternMass (fun xy : (Fin N × I → Binary) × (Fin N × J → Binary) => |
| 51 | α xy.1*β xy.2) (crossBits C N) target- |
| 52 | (∑ x,α x*f x)*(∑ y,β y*g y)| ≤ |
| 53 | (2 : ℝ)^(Fintype.card S+2)*(C₁*C₂/Real.sqrt ((2 : ℝ)^N)) |
| 54 | |
| 55 | end Lax342547.CrossBatchMixing |
| 56 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments