OAI/NumberTheory/PiExponent/Approximation/
1051 declarations, 0 contain sorry, 0 declared as axioms; 133 files
Files
- AddEquivSignedSum.lean 2 declarations
- AdditiveKernelTransport.lean 4 declarations
- AdmissibleMatrixFrame.lean 3 declarations
- AdmissibleMatrixGeometry.lean 3 declarations
- AdmissibleMatrixInterpolation.lean 11 declarations
- AdmissibleParameters.lean 22 declarations
- AffineClosedAnnihilatedDescent.lean 9 declarations
- AffineThickeningCriterion.lean 4 declarations
- ApproximationCenters.lean 9 declarations
- ApproximationSelection.lean 1 declarations
- Arithmetic.lean 28 declarations
- CanonicalAffineRecovery.lean 3 declarations
- ClosedAnnihilatedDescent.lean 10 declarations
- ClosedImmersionModules.lean 9 declarations
- ClosedImmersionSerreTransfer.lean 10 declarations
- ClosedPowerSectionLifting.lean 1 declarations
- ClosedPullbackUnit.lean 12 declarations
- ClosedPullbackUnitRestriction.lean 4 declarations
- ClosedPushforwardAffine.lean 5 declarations
- ClosedPushforwardCoherent.lean 7 declarations
- ClosedPushforwardLinear.lean 13 declarations
- ClosedRestrictionTensor.lean 12 declarations
- ClosedSectionLifting.lean 2 declarations
- ClosedSupportedSerre.lean 3 declarations
- ClosedThickeningSections.lean 4 declarations
- ClosedUnitKernel.lean 4 declarations
- CocycleTensor.lean 11 declarations
- CocycleTensorIso.lean 4 declarations
- CoherentCokernels.lean 5 declarations
- CoherentTwistPresentation.lean 34 declarations
- Comparison.lean 2 declarations
- CompositePullbackFrame.lean 4 declarations
- ConstantPullbackDegree.lean 5 declarations
- CoordinateFrameIdentification.lean 2 declarations
- CoordinateSliceComparison.lean 12 declarations
- DeterminantContradiction.lean 23 declarations
- Exponent.lean 7 declarations
- FibreNormalRigidity.lean 3 declarations
- FibreWeightSeparation.lean 1 declarations
- FormalMatrixBridge.lean 9 declarations
- FormalMatrixSurjectivity.lean 2 declarations
- FrameEquationFamily.lean 13 declarations
- FrameResidueDirections.lean 1 declarations
- FrameSections.lean 15 declarations
- FrameSubopens.lean 3 declarations
- FrameSubopensCoherence.lean 2 declarations
- FrameTensorPowers.lean 9 declarations
- FramedPullback.lean 4 declarations
- FullSupportNilpotence.lean 5 declarations
- GeneratorsSectionCover.lean 12 declarations
- GenericFibreRigidity.lean 5 declarations
- GenericNormalRigidity.lean 2 declarations
- GlobalClosedAnnihilatedDescent.lean 5 declarations
- GlobalSectionClearing.lean 41 declarations
- GlueGlobalGenerators.lean 4 declarations
- IntegralLineSections.lean 12 declarations
- InterpolationConsequence.lean 3 declarations
- InterpolationMatrix.lean 25 declarations
- InverseDualRestriction.lean 3 declarations
- InverseFrameRestriction.lean 6 declarations
- InverseFrames.lean 15 declarations
- LineClosedUnit.lean 4 declarations
- LinePowerLaws.lean 9 declarations
- LinePullback.lean 3 declarations
- LinePullbackPowers.lean 11 declarations
- MatrixArithmetic.lean 38 declarations
- MatrixCounting.lean 9 declarations
- MatrixTranslation.lean 21 declarations
- MatrixTranslationBounds.lean 12 declarations
- MixedFrameExtension.lean 2 declarations
- MixedSectionExtension.lean 3 declarations
- MixedSectionOpenExtension.lean 1 declarations
- ModuleLinePowerLaws.lean 7 declarations
- ModulePullbackCoherent.lean 2 declarations
- NegativeTwistPresentations.lean 9 declarations
- NoetherianPowerExtension.lean 2 declarations
- NumericalMarginRestriction.lean 6 declarations
- NumericalSlopeInduction.lean 4 declarations
- NumericalThresholdStep.lean 1 declarations
- OpenBaseChange.lean 6 declarations
- OpenPullbackUnit.lean 2 imports, no declarations
- OrdinaryComponentRigidity.lean 4 declarations
- OrdinarySliceComparison.lean 1 declarations
- Parameters.lean 12 declarations
- PersistentComponents.lean 10 declarations
- PersistentWeightComparison.lean 7 declarations
- PowerSectionExtension.lean 8 declarations
- ProjectionFormula.lean 11 declarations
- PushforwardOpenSections.lean 7 declarations
- PushforwardSectionComparison.lean 7 declarations
- PushforwardTensor.lean 8 declarations
- RectangularVolume.lean 7 declarations
- RegularComponentSection.lean 4 declarations
- RegularSectionChoice.lean 9 declarations
- RegularSectionMono.lean 4 declarations
- RowTranslation.lean 35 declarations
- SectionDivision.lean 5 declarations
- SectionImageSupport.lean 3 declarations
- SectionOpens.lean 15 declarations
- SectionPowerFrames.lean 9 declarations
- SectionPowerOpens.lean 5 declarations
- SectionPullback.lean 2 declarations
- SectionZeroSupport.lean 2 declarations
- SerreAssembly.lean 3 declarations
- SerrePowerDescent.lean 5 declarations
- SerreSectionLifting.lean 2 declarations
- Sigma.lean 1 declarations
- SuccessiveApproximations.lean 9 declarations
- TensorMixedSection.lean 8 declarations
- TensorOpenBaseChange.lean 7 declarations
- TensorPowerRestriction.lean 7 declarations
- TensorPure.lean 18 declarations
- TensorSectionOpen.lean 7 declarations
- TwistGlobalExtension.lean 8 declarations
- TwistPowerSection.lean 3 declarations
- TwistPresentations.lean 13 declarations
- TwistSectionClearing.lean 10 declarations
- TwistSectionScalars.lean 6 declarations
- TwistSections.lean 10 declarations
- WeightErrorMargin.lean 4 declarations
- WeightSeparation.lean 7 declarations
- WeightSeparationConstant.lean 4 declarations
- WeightSeparationProducts.lean 2 declarations
- WeightedAffineParametrization.lean 5 declarations
- WeightedCompactification.lean 17 declarations
- WeightedCompactificationGeometry.lean 5 declarations
- WeightedCompactificationImmersion.lean 4 declarations
- WeightedFrameDegree.lean 2 declarations
- WeightedGeometryScale.lean 19 declarations
- WeightedGlobalSectionBound.lean 2 declarations
- WeightedPullbackDegree.lean 1 declarations
- WeightedSectionOrder.lean 9 declarations
- WeightedSliceDegree.lean 24 declarations