diff --git a/Complexity.lean b/Complexity.lean index d76bc905b5..d9ed155f64 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1597,6 +1597,7 @@ public import Complexity.Foundations.Data.BitString.Multiplication public import Complexity.Foundations.Data.BitString.PackedCount public import Complexity.Foundations.Data.BitString.Packing public import Complexity.Foundations.Data.BitString.Parity +public import Complexity.Foundations.Data.BitString.Parity.Weight public import Complexity.Foundations.Data.BitString.PartialAssignment public import Complexity.Foundations.Data.BitString.Point public import Complexity.Foundations.Data.BitString.Projection diff --git a/Complexity/Computability/Circuit/Boolean/FanInTwo.lean b/Complexity/Computability/Circuit/Boolean/FanInTwo.lean index b7fba49385..1e7d997cf7 100644 --- a/Complexity/Computability/Circuit/Boolean/FanInTwo.lean +++ b/Complexity/Computability/Circuit/Boolean/FanInTwo.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Circuit.Boolean.DepthClasses public import Complexity.Computability.Circuit.Boolean.Formula public import Complexity.Computability.Circuit.MapLines public import Complexity.Computability.Circuit.SimulationDepth +import Mathlib.Algebra.BigOperators.Fin import Complexity.Computability.Circuit.Program import Complexity.Computability.Circuit.Simulation import Complexity.Foundations.Data.Nat.PolynomialBound.Log diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean index ef9b193440..c6c8e2eb18 100644 --- a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean +++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Circuit.Boolean.FirstOrder public import Mathlib.Order.Filter.AtTopBot.Defs public import Mathlib.SetTheory.Cardinal.Finite +import Mathlib.Algebra.BigOperators.Fin import Complexity.Computability.Circuit.Boolean.Hastad import Complexity.Foundations.Data.Nat.PolynomialBound.Closure import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential diff --git a/Complexity/Computability/Circuit/Boolean/HardCore.lean b/Complexity/Computability/Circuit/Boolean/HardCore.lean index 82a0cc522c..31661e0f79 100644 --- a/Complexity/Computability/Circuit/Boolean/HardCore.lean +++ b/Complexity/Computability/Circuit/Boolean/HardCore.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Circuit.Boolean.AtLeast public import Complexity.Computability.Circuit.Boolean.Synthesis public import Mathlib.Basic.Real.Basic +import Complexity.Foundations.Data.BitString.Basic import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Potential import Mathlib.Algebra.BigOperators.Fin import Mathlib.Algebra.Order.BigOperators.Group.Finset diff --git a/Complexity/Computability/Circuit/Boolean/HardnessAmplification/WorstCase.lean b/Complexity/Computability/Circuit/Boolean/HardnessAmplification/WorstCase.lean index 401ea6191c..3399e12957 100644 --- a/Complexity/Computability/Circuit/Boolean/HardnessAmplification/WorstCase.lean +++ b/Complexity/Computability/Circuit/Boolean/HardnessAmplification/WorstCase.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Circuit.Boolean.HardnessAmplification.Sta public import Complexity.Foundations.BooleanAnalysis.Hadamard public import Complexity.Foundations.Data.Code.Concatenation public import Complexity.Foundations.Data.Code.LowDegreeExtension +import Complexity.Foundations.Data.BitString.Basic import Mathlib.Tactic.Linarith import Mathlib.Tactic.NormNum import Mathlib.Tactic.Positivity diff --git a/Complexity/Computability/Circuit/Boolean/Majority.lean b/Complexity/Computability/Circuit/Boolean/Majority.lean index 80673a57fb..1a14c7b56e 100644 --- a/Complexity/Computability/Circuit/Boolean/Majority.lean +++ b/Complexity/Computability/Circuit/Boolean/Majority.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Circuit.Boolean.AC0 public import Complexity.Foundations.Data.BitString.Weight +import Complexity.Foundations.Data.BitString.Parity.Weight import Complexity.Foundations.Data.Fin.Append import Mathlib.Data.Fintype.Fin diff --git a/Complexity/Computability/Circuit/Boolean/Multiplicity.lean b/Complexity/Computability/Circuit/Boolean/Multiplicity.lean index e61f8550e8..c8f85c2630 100644 --- a/Complexity/Computability/Circuit/Boolean/Multiplicity.lean +++ b/Complexity/Computability/Circuit/Boolean/Multiplicity.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Circuit.Boolean.FanInTwo +import Mathlib.Algebra.BigOperators.Fin /-! # Symmetric gates reading their wires with multiplicities diff --git a/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean b/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean index 2d3a3865d1..62d60cd21d 100644 --- a/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean +++ b/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Circuit.Boolean.ConstDepth public import Complexity.Computability.Circuit.Boolean.Threshold public import Complexity.Computability.Circuit.Simulation +public import Complexity.Foundations.Data.BitString.Parity.Weight import Mathlib.Algebra.BigOperators.Fin /-! diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean index 6504fa438a..2de5970b13 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean @@ -9,6 +9,7 @@ module public import Complexity.Init public import Complexity.Computability.Circuit.Boolean.WeightedThreshold.CapacityCircuit +import Mathlib.Algebra.BigOperators.Fin import Mathlib.Data.Int.Interval import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean index 0b1c0b0b8d..6d63cd7441 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean @@ -10,6 +10,7 @@ module public import Complexity.Init public import Complexity.Computability.Circuit.Boolean.WeightedThreshold.CapacityCircuit public import Complexity.Foundations.BooleanAnalysis.Hadamard +import Mathlib.Algebra.BigOperators.Fin /-! # Pending-bias state simulation and input-summary lower bounds for threshold circuits diff --git a/Complexity/Computability/Circuit/Boolean/XorLemma.lean b/Complexity/Computability/Circuit/Boolean/XorLemma.lean index fd15627d2c..5c64f60335 100644 --- a/Complexity/Computability/Circuit/Boolean/XorLemma.lean +++ b/Complexity/Computability/Circuit/Boolean/XorLemma.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Circuit.Boolean.HardCore public import Complexity.Foundations.Data.BitString.Block public import Complexity.Foundations.Data.BitString.Parity +import Complexity.Foundations.Data.BitString.Basic import Complexity.Computability.Circuit.Boolean.Substitution import Mathlib.Algebra.BigOperators.Ring.Finset import Mathlib.Algebra.Order.BigOperators.Group.Finset diff --git a/Complexity/Computability/Complexity/AffineDisperser/Program.lean b/Complexity/Computability/Complexity/AffineDisperser/Program.lean index 3661fec5ea..b3801a8fb8 100644 --- a/Complexity/Computability/Complexity/AffineDisperser/Program.lean +++ b/Complexity/Computability/Complexity/AffineDisperser/Program.lean @@ -11,6 +11,7 @@ public import Complexity.Init public import Complexity.Computability.Complexity.AffineDisperser.BinaryPolynomial public import Complexity.Computability.Complexity.AffineDisperser.Coordinates public import Complexity.Foundations.Combinatorics.AffineDisperser.Explicit +import Mathlib.Algebra.BigOperators.Fin import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/PCP/AssignmentTester.lean b/Complexity/Computability/PCP/AssignmentTester.lean index 6c9bb5c6ca..1e2b3e32f2 100644 --- a/Complexity/Computability/PCP/AssignmentTester.lean +++ b/Complexity/Computability/PCP/AssignmentTester.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.PCP.LocalTest public import Complexity.Foundations.BooleanAnalysis.HadamardTester public import Mathlib.Data.Fin.VecNotation +import Mathlib.Algebra.BigOperators.Fin import Complexity.Foundations.Data.Finset.Expect import Complexity.Foundations.Data.Hamming import Mathlib.Algebra.Order.BigOperators.Expect diff --git a/Complexity/Crypto/Computational/GoldreichLevin/Nonuniform.lean b/Complexity/Crypto/Computational/GoldreichLevin/Nonuniform.lean index da88a01d8f..b8050e4bbe 100644 --- a/Complexity/Crypto/Computational/GoldreichLevin/Nonuniform.lean +++ b/Complexity/Crypto/Computational/GoldreichLevin/Nonuniform.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Crypto.Computational.GoldreichLevin.Decoding +import Complexity.Foundations.Data.BitString.Basic import Mathlib.Probability.ProbabilityMassFunction.Integrals /-! diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean index 3d136d1caa..8209a58c58 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized +import Mathlib.Algebra.BigOperators.Fin import Complexity.Foundations.Data.List.Basic /-! diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean index 658e1b64c7..fa1cc895ef 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean @@ -9,6 +9,7 @@ module public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption +import Mathlib.Algebra.BigOperators.Fin import Complexity.Foundations.Data.List.Basic import Complexity.Foundations.Data.Nat.Bits diff --git a/Complexity/Foundations/BooleanAnalysis/Convolution.lean b/Complexity/Foundations/BooleanAnalysis/Convolution.lean index 4a9aeed349..8a2b75d8da 100644 --- a/Complexity/Foundations/BooleanAnalysis/Convolution.lean +++ b/Complexity/Foundations/BooleanAnalysis/Convolution.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Foundations.BooleanAnalysis.Fourier +import Complexity.Foundations.Data.BitString.Basic import Complexity.Foundations.Data.Finset.Expect import Mathlib.Tactic.Ring diff --git a/Complexity/Foundations/BooleanAnalysis/PolynomialCorrelation.lean b/Complexity/Foundations/BooleanAnalysis/PolynomialCorrelation.lean index 780cef5ebc..c1d53cb843 100644 --- a/Complexity/Foundations/BooleanAnalysis/PolynomialCorrelation.lean +++ b/Complexity/Foundations/BooleanAnalysis/PolynomialCorrelation.lean @@ -14,6 +14,7 @@ public import Complexity.Foundations.Data.BitString.Weight public import Mathlib.Analysis.Real.Sqrt public import Mathlib.Data.ZMod.Defs public import Mathlib.Logic.Equiv.Fin.Basic +import Complexity.Foundations.Data.BitString.Basic import Complexity.Foundations.Combinatorics.CentralBinomial import Mathlib.Algebra.CharP.Two import Mathlib.Algebra.Field.ZMod diff --git a/Complexity/Foundations/Data/BitString/Hamming.lean b/Complexity/Foundations/Data/BitString/Hamming.lean index 37b7307724..ec4b5ac8e3 100644 --- a/Complexity/Foundations/Data/BitString/Hamming.lean +++ b/Complexity/Foundations/Data/BitString/Hamming.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Foundations.Data.BitString.Weight +public import Complexity.Foundations.Data.BitString.Parity /-! # The Hamming geometry of the Boolean cube diff --git a/Complexity/Foundations/Data/BitString/List/Operations.lean b/Complexity/Foundations/Data/BitString/List/Operations.lean index cd2fc83025..78a2790de1 100644 --- a/Complexity/Foundations/Data/BitString/List/Operations.lean +++ b/Complexity/Foundations/Data/BitString/List/Operations.lean @@ -10,6 +10,7 @@ module public import Complexity.Foundations.Data.BitString.List public import Complexity.Foundations.Data.BitString.Weight public import Mathlib.Data.Matrix.Mul +import Mathlib.Algebra.BigOperators.Fin /-! # Algebraic operations on lists of bits diff --git a/Complexity/Foundations/Data/BitString/Parity.lean b/Complexity/Foundations/Data/BitString/Parity.lean index 7bc9d6f632..d43c8ec0a1 100644 --- a/Complexity/Foundations/Data/BitString/Parity.lean +++ b/Complexity/Foundations/Data/BitString/Parity.lean @@ -7,7 +7,8 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Foundations.Data.BitString.Basic +public import Cslib.Foundations.Data.BitString +public import Mathlib.Algebra.Ring.BooleanRing public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Algebra.Group.Hom.Defs public import Mathlib.Data.Finset.Card @@ -19,7 +20,6 @@ public import Mathlib.Data.Fintype.Pi public import Mathlib.Logic.Function.Const public import Mathlib.Logic.Function.DependsOn import Mathlib.Algebra.BigOperators.Ring.Finset -import Mathlib.Algebra.Ring.BooleanRing import Mathlib.Data.Fintype.BigOperators import Mathlib.GroupTheory.Index @@ -34,7 +34,7 @@ In the Boolean ring `Bool`, where `a + b = (a ^^ b)`, the parity on `s` is the s `s` (`parityOn_eq_sum`), so it splits over disjoint unions (`parityOn_union`), the parity on a symmetric difference is the exclusive or of the parities (`parityOn_symmDiff`), and it is additive for the coordinatewise sum of bit strings (`parityOn_add`, bundled as `parityOnAddMonoidHom`). Bit -strings are added with `+`, under which each is its own negative (`BitString.add_self`), and +strings are added with `+`, under which each is its own negative (`BooleanRing.add_self`), and single bits with `^^`. Flipping one of the bits negates the parity (`parityOn_update_not`), so the parity of a nonempty set of bits is not constant and depends on each of them; being additive, it then takes each value on exactly half of the inputs (`card_filter_parityOn_eq`). diff --git a/Complexity/Foundations/Data/BitString/Parity/Weight.lean b/Complexity/Foundations/Data/BitString/Parity/Weight.lean new file mode 100644 index 0000000000..7754a10939 --- /dev/null +++ b/Complexity/Foundations/Data/BitString/Parity/Weight.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.BitString.Parity +public import Complexity.Foundations.Data.BitString.Weight + +/-! +# Parity and Hamming weight + +The parity of a bit string is the parity of its Hamming weight (`Cslib.parity_eq_decide_weight`), +so parity is a symmetric Boolean function (`Cslib.isSymmetric_parity`). This bridge is kept apart +from both `BitString.Parity` and `BitString.Weight`, so that neither of them imports the other. + +## Main results + +* `Cslib.parity_eq_decide_weight`: parity is the parity of the weight. +* `Cslib.isSymmetric_parity`: parity is symmetric. +-/ + +@[expose] public section + +namespace Cslib + +/-- Parity is the parity of the weight. -/ +theorem parity_eq_decide_weight {n : ℕ} (x : BitString n) : + parity n x = decide (BitString.weight x % 2 = 1) := + rfl + +/-- Parity is symmetric. -/ +theorem isSymmetric_parity {n : ℕ} : (parity n).IsSymmetric := fun x y h => by + simp only [BitString.weight] at h + simp only [parity, parityOn, h] + +end Cslib diff --git a/Complexity/Foundations/Data/BitString/Weight.lean b/Complexity/Foundations/Data/BitString/Weight.lean index 3650232217..41dc6a2073 100644 --- a/Complexity/Foundations/Data/BitString/Weight.lean +++ b/Complexity/Foundations/Data/BitString/Weight.lean @@ -7,7 +7,8 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Foundations.Data.BitString.Parity +public import Cslib.Foundations.Data.BitString +public import Mathlib.Algebra.Ring.BooleanRing public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Data.Fintype.Sum public import Mathlib.Data.Nat.Choose.Basic @@ -48,8 +49,7 @@ function is *symmetric* when it depends only on the weight of its input * `Cslib.strictMajority_not`: strict majority of the negated bits is the negation of majority. * `Cslib.BitString.strictMajorityOn`: strict majority on a finite set of voting indices. * `Cslib.le_card_ne_of_strictMajority_ne`: a wrong majority requires at least half wrong votes. -* `Cslib.isSymmetric_threshold`, `Cslib.isSymmetric_parity`: threshold functions and parity are - symmetric. +* `Cslib.isSymmetric_threshold`: threshold functions are symmetric. ## References @@ -354,13 +354,4 @@ theorem isSymmetric_majority : (majority n).IsSymmetric := theorem isSymmetric_strictMajority : (strictMajority n).IsSymmetric := isSymmetric_threshold _ -/-- Parity is the parity of the weight. -/ -theorem parity_eq_decide_weight (x : BitString n) : parity n x = decide (weight x % 2 = 1) := - rfl - -/-- Parity is symmetric. -/ -theorem isSymmetric_parity : (parity n).IsSymmetric := fun x y h => by - simp only [weight] at h - simp only [parity, parityOn, h] - end Cslib diff --git a/Complexity/Languages/Probabilistic/Repeat.lean b/Complexity/Languages/Probabilistic/Repeat.lean index e4468fa355..588e4a1c16 100644 --- a/Complexity/Languages/Probabilistic/Repeat.lean +++ b/Complexity/Languages/Probabilistic/Repeat.lean @@ -10,6 +10,7 @@ module public import Complexity.Languages.Probabilistic.Basic public import Complexity.Probability.BitString.List public import Complexity.Probability.Product +import Mathlib.Algebra.BigOperators.Fin /-! # Bounded repetition of probabilistic programs diff --git a/Complexity/Logics/Propositional/CNF/Parity.lean b/Complexity/Logics/Propositional/CNF/Parity.lean index cb86e121d1..4ae9132347 100644 --- a/Complexity/Logics/Propositional/CNF/Parity.lean +++ b/Complexity/Logics/Propositional/CNF/Parity.lean @@ -9,6 +9,7 @@ module public import Complexity.Foundations.Data.BitString.Parity public import Complexity.Logics.Propositional.CNF +public import Mathlib.Data.Finset.Powerset /-! # Parity constraints in conjunctive normal form diff --git a/ComplexityTests/HardnessAmplification.lean b/ComplexityTests/HardnessAmplification.lean index e17fc107de..b8bf94dfbf 100644 --- a/ComplexityTests/HardnessAmplification.lean +++ b/ComplexityTests/HardnessAmplification.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Complexity.Foundations.Data.BitString.Basic import Complexity.Computability.Circuit.Boolean.XorLemma /-! Impagliazzo's hard-core lemma and Yao's XOR lemma: a concrete hard-core measure, the diff --git a/ComplexityTests/HastadSharp.lean b/ComplexityTests/HastadSharp.lean index 5604d4efd5..f6ded626cf 100644 --- a/ComplexityTests/HastadSharp.lean +++ b/ComplexityTests/HastadSharp.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Complexity.Foundations.Data.BitString.Parity.Weight import Complexity.Computability.Circuit.Boolean.Hastad.Sharp import Complexity.Computability.Circuit.Boolean.FirstOrder.Parity import Complexity.Computability.Circuit.Boolean.ShallowSymmetric diff --git a/ComplexityTests/QueryComplexity/Randomized.lean b/ComplexityTests/QueryComplexity/Randomized.lean index 66f15da4b2..8f81c76472 100644 --- a/ComplexityTests/QueryComplexity/Randomized.lean +++ b/ComplexityTests/QueryComplexity/Randomized.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Mathlib.Algebra.BigOperators.Fin import Complexity.Computability.QueryComplexity.ApproximateDegree.Or import Complexity.Computability.QueryComplexity.Randomized.Nisan import Complexity.Computability.QueryComplexity.Yao diff --git a/ComplexityTests/QueryComplexity/Sensitivity.lean b/ComplexityTests/QueryComplexity/Sensitivity.lean index 0c3343bdf5..6e96201b58 100644 --- a/ComplexityTests/QueryComplexity/Sensitivity.lean +++ b/ComplexityTests/QueryComplexity/Sensitivity.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Complexity.Foundations.Data.BitString.Parity.Weight import Complexity.Computability.DecisionTree.Symmetric import Complexity.Computability.QueryComplexity.Monotone import Complexity.Computability.QueryComplexity.SensitivityBounds diff --git a/ComplexityTests/ThresholdCapacityCircuit.lean b/ComplexityTests/ThresholdCapacityCircuit.lean index 6e063e7465..56598e8385 100644 --- a/ComplexityTests/ThresholdCapacityCircuit.lean +++ b/ComplexityTests/ThresholdCapacityCircuit.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Mathlib.Algebra.BigOperators.Fin import Complexity.Computability.Circuit.Boolean.WeightedThreshold.CapacityCircuit import Mathlib.Data.Fintype.Powerset import Mathlib.Tactic.FinCases diff --git a/ComplexityTests/ThresholdInnerProduct.lean b/ComplexityTests/ThresholdInnerProduct.lean index 2de3d8f9bb..12538affb0 100644 --- a/ComplexityTests/ThresholdInnerProduct.lean +++ b/ComplexityTests/ThresholdInnerProduct.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Mathlib.Algebra.BigOperators.Fin import Complexity.Foundations.BooleanAnalysis.HadamardRectangles import Complexity.Computability.DecisionTree.InnerProduct import Mathlib.Data.Fintype.Powerset