OAI/NumberTheory/TwoPoint/Circuits/
438 declarations, 0 contain sorry, 0 declared as axioms; 72 files
Files
- BitEncoding.lean 13 declarations
- BitMarginals.lean 12 declarations
- BravermanDepth22Theorem.lean 1 declarations
- CircuitAndCertificate.lean 1 declarations
- CircuitApproximationComparison.lean 2 declarations
- CircuitApproximationDegree.lean 3 declarations
- CircuitAssignmentUpdates.lean 7 declarations
- CircuitBernoulli.lean 6 declarations
- CircuitBlockCode.lean 9 declarations
- CircuitBooleanOps.lean 12 declarations
- CircuitBravermanApproximation.lean 1 declarations
- CircuitCanonicalTree.lean 6 declarations
- CircuitCertificateBounds.lean 6 declarations
- CircuitCertifiedGate.lean 5 declarations
- CircuitClauseIndependence.lean 5 declarations
- CircuitComparison.lean 11 declarations
- CircuitDecisionDNF.lean 12 declarations
- CircuitDecisionRestriction.lean 8 declarations
- CircuitDecisionTree.lean 7 declarations
- CircuitDegreeBound.lean 1 declarations
- CircuitDepthSwitching.lean 2 declarations
- CircuitDyadicApproximation.lean 4 declarations
- CircuitDyadicBudgets.lean 11 declarations
- CircuitDyadicComparison.lean 2 declarations
- CircuitDyadicErrors.lean 4 declarations
- CircuitDyadicSampling.lean 1 declarations
- CircuitEncoding.lean 19 declarations
- CircuitErrorCutoff.lean 7 declarations
- CircuitExceptionBudget.lean 2 declarations
- CircuitFiniteCodes.lean 9 declarations
- CircuitFourierDegree.lean 4 declarations
- CircuitFourierSwitching.lean 2 declarations
- CircuitFourierTruncation.lean 5 declarations
- CircuitGateApproximation.lean 3 declarations
- CircuitGateComposition.lean 1 declarations
- CircuitGateFailure.lean 10 declarations
- CircuitGateSwitching.lean 5 declarations
- CircuitIsolation.lean 6 declarations
- CircuitIsolationEvent.lean 13 declarations
- CircuitLogarithmicBudget.lean 2 declarations
- CircuitMixedLaw.lean 6 declarations
- CircuitNormBudget.lean 1 declarations
- CircuitOrApproximation.lean 3 declarations
- CircuitOrCertificate.lean 2 declarations
- CircuitPartialAssignment.lean 20 declarations
- CircuitPolynomialAlgebra.lean 7 declarations
- CircuitPolynomialGrowth.lean 8 declarations
- CircuitPolynomialMean.lean 11 declarations
- CircuitProbabilisticMethod.lean 2 declarations
- CircuitQueryWalk.lean 9 declarations
- CircuitRandomGate.lean 9 declarations
- CircuitRandomRestriction.lean 4 declarations
- CircuitRecursiveApproximation.lean 1 declarations
- CircuitRestriction.lean 3 declarations
- CircuitRestrictionComposition.lean 5 declarations
- CircuitRestrictionDecay.lean 3 declarations
- CircuitRestrictionDistribution.lean 6 declarations
- CircuitRestrictionFourier.lean 4 declarations
- CircuitRestrictionLaw.lean 4 declarations
- CircuitRestrictionProbability.lean 4 declarations
- CircuitRestrictionSurvival.lean 2 declarations
- CircuitSampleNorm.lean 2 declarations
- CircuitSamplingException.lean 8 declarations
- CircuitSamplingGrid.lean 4 declarations
- CircuitSemiExact.lean 5 declarations
- CircuitSwitchingLemma.lean 3 declarations
- CircuitSwitchingMass.lean 1 declarations
- CircuitTreeWalk.lean 4 declarations
- CircuitWalkCode.lean 5 declarations
- CircuitWalkImage.lean 10 declarations
- CircuitWalshExpansion.lean 3 declarations
- FourierCorrection.lean 39 declarations