From 0e37c3b26fe9d98b156b0213c4bf7bdd28dca739 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 07:08:58 +0000 Subject: [PATCH] refactor(boolean-analysis): move Hypercube and Symmetrization to Foundations/BooleanAnalysis (#610) Move `Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean` to `Complexity/Foundations/BooleanAnalysis/Hypercube.lean` and `Complexity/Computability/QueryComplexity/Symmetrization.lean` to `Complexity/Foundations/BooleanAnalysis/Symmetrization.lean`. Both modules live in `namespace Cslib.BitString` and depend only on `Complexity/Foundations/BooleanAnalysis/`, `Complexity/Foundations/Data/BitString/Weight.lean`, and Mathlib. Co-authored-by: Jetski --- Complexity.lean | 4 ++-- .../Computability/QueryComplexity/ApproximateDegree/Or.lean | 2 +- Complexity/Computability/QueryComplexity/Huang.lean | 2 +- Complexity/Computability/QueryComplexity/NisanSzegedy.lean | 2 +- .../BooleanAnalysis}/Hypercube.lean | 0 .../BooleanAnalysis}/Symmetrization.lean | 0 ComplexityTests/QueryComplexity/Approximate.lean | 2 +- 7 files changed, 6 insertions(+), 6 deletions(-) rename Complexity/{Computability/QueryComplexity/Sensitivity => Foundations/BooleanAnalysis}/Hypercube.lean (100%) rename Complexity/{Computability/QueryComplexity => Foundations/BooleanAnalysis}/Symmetrization.lean (100%) diff --git a/Complexity.lean b/Complexity.lean index e34b9456ee..3c77f39a05 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1195,7 +1195,6 @@ public import Complexity.Computability.QueryComplexity.Randomized public import Complexity.Computability.QueryComplexity.Randomized.Nisan public import Complexity.Computability.QueryComplexity.Relations public import Complexity.Computability.QueryComplexity.Restriction -public import Complexity.Computability.QueryComplexity.Sensitivity.Hypercube public import Complexity.Computability.QueryComplexity.SensitivityBounds public import Complexity.Computability.QueryComplexity.SensitivitySeparation public import Complexity.Computability.QueryComplexity.SensitivitySeparation.Internal.Basic @@ -1241,7 +1240,6 @@ public import Complexity.Computability.QueryComplexity.SensitivitySeparation.Int public import Complexity.Computability.QueryComplexity.SensitivitySeparation.Internal.TournamentCyclic public import Complexity.Computability.QueryComplexity.SensitivitySeparation.Internal.Tower public import Complexity.Computability.QueryComplexity.SensitivitySeparation.Internal.TowerProfiles -public import Complexity.Computability.QueryComplexity.Symmetrization public import Complexity.Computability.QueryComplexity.Threshold public import Complexity.Computability.QueryComplexity.Yao public import Complexity.Computability.RAM.Cost @@ -1514,6 +1512,7 @@ public import Complexity.Foundations.BooleanAnalysis.Hypercontractivity.Derivati public import Complexity.Foundations.BooleanAnalysis.Hypercontractivity.LpNorm public import Complexity.Foundations.BooleanAnalysis.Hypercontractivity.Tensorization public import Complexity.Foundations.BooleanAnalysis.Hypercontractivity.TwoPoint +public import Complexity.Foundations.BooleanAnalysis.Hypercube public import Complexity.Foundations.BooleanAnalysis.Influence public import Complexity.Foundations.BooleanAnalysis.KahnKalaiLinial public import Complexity.Foundations.BooleanAnalysis.LightPatterns @@ -1528,6 +1527,7 @@ public import Complexity.Foundations.BooleanAnalysis.Noise public import Complexity.Foundations.BooleanAnalysis.PolynomialCorrelation public import Complexity.Foundations.BooleanAnalysis.RelevantCoordinates public import Complexity.Foundations.BooleanAnalysis.SignApproximation +public import Complexity.Foundations.BooleanAnalysis.Symmetrization public import Complexity.Foundations.Combinatorics.AffineDisperser public import Complexity.Foundations.Combinatorics.AffineDisperser.AffineSubspace public import Complexity.Foundations.Combinatorics.AffineDisperser.BinaryField diff --git a/Complexity/Computability/QueryComplexity/ApproximateDegree/Or.lean b/Complexity/Computability/QueryComplexity/ApproximateDegree/Or.lean index 694404c67b..c2cefe45a7 100644 --- a/Complexity/Computability/QueryComplexity/ApproximateDegree/Or.lean +++ b/Complexity/Computability/QueryComplexity/ApproximateDegree/Or.lean @@ -10,7 +10,7 @@ module public import Complexity.Computability.QueryComplexity.NisanSzegedy public import Complexity.Computability.QueryComplexity.Threshold public import Mathlib.RingTheory.Polynomial.Chebyshev -import Complexity.Computability.QueryComplexity.Symmetrization +import Complexity.Foundations.BooleanAnalysis.Symmetrization import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema /-! diff --git a/Complexity/Computability/QueryComplexity/Huang.lean b/Complexity/Computability/QueryComplexity/Huang.lean index d2c3afb901..bbf539c426 100644 --- a/Complexity/Computability/QueryComplexity/Huang.lean +++ b/Complexity/Computability/QueryComplexity/Huang.lean @@ -8,7 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.QueryComplexity.Degree -public import Complexity.Computability.QueryComplexity.Sensitivity.Hypercube +public import Complexity.Foundations.BooleanAnalysis.Hypercube public import Cslib.Computability.QueryComplexity.Measures /-! diff --git a/Complexity/Computability/QueryComplexity/NisanSzegedy.lean b/Complexity/Computability/QueryComplexity/NisanSzegedy.lean index c5bbae6322..1c042854bf 100644 --- a/Complexity/Computability/QueryComplexity/NisanSzegedy.lean +++ b/Complexity/Computability/QueryComplexity/NisanSzegedy.lean @@ -10,8 +10,8 @@ module public import Complexity.Computability.QueryComplexity.ApproximateDegree public import Complexity.Computability.QueryComplexity.Huang public import Complexity.Computability.QueryComplexity.Relations -import Complexity.Computability.QueryComplexity.Symmetrization import Complexity.Foundations.Analysis.MarkovInequality +import Complexity.Foundations.BooleanAnalysis.Symmetrization import Mathlib.Algebra.Order.BigOperators.Expect import Mathlib.Analysis.Calculus.Deriv.MeanValue import Mathlib.Analysis.Calculus.Deriv.Polynomial diff --git a/Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean b/Complexity/Foundations/BooleanAnalysis/Hypercube.lean similarity index 100% rename from Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean rename to Complexity/Foundations/BooleanAnalysis/Hypercube.lean diff --git a/Complexity/Computability/QueryComplexity/Symmetrization.lean b/Complexity/Foundations/BooleanAnalysis/Symmetrization.lean similarity index 100% rename from Complexity/Computability/QueryComplexity/Symmetrization.lean rename to Complexity/Foundations/BooleanAnalysis/Symmetrization.lean diff --git a/ComplexityTests/QueryComplexity/Approximate.lean b/ComplexityTests/QueryComplexity/Approximate.lean index d09aea17d5..b32d9b6fbd 100644 --- a/ComplexityTests/QueryComplexity/Approximate.lean +++ b/ComplexityTests/QueryComplexity/Approximate.lean @@ -5,8 +5,8 @@ Authors: Samuel Schlesinger -/ import Complexity.Computability.QueryComplexity.ApproximateDegree.Or -import Complexity.Computability.QueryComplexity.Symmetrization import Complexity.Foundations.Analysis.MarkovInequality +import Complexity.Foundations.BooleanAnalysis.Symmetrization import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema /-! Markov's inequality and its discrete forms, Minsky–Papert symmetrization, approximate degree