`OAI/Analysis/AffineBernstein/`

1666 declarations, 0 contain sorry, 0 declared as axioms; 326 files

Files

ABPCriticalDensity.lean 1 declarations
ABPMatrix.lean 8 declarations
ActualAmbientFEquation.lean 2 declarations
ActualAngularSupport.lean 5 declarations
ActualAreaMass.lean 1 declarations
ActualBaseCurvature.lean 6 declarations
ActualBaseMinors.lean 7 declarations
ActualChartArea.lean 2 declarations
ActualConormalScale.lean 1 declarations
ActualFiberArea.lean 2 declarations
ActualFlatFEquation.lean 1 declarations
ActualFlatInverse.lean 3 declarations
ActualFlatWeakEuler.lean 1 declarations
ActualGlobalAngular.lean 1 declarations
ActualGlobalBase.lean 1 declarations
ActualGlobalCoercive.lean 8 declarations
ActualGlobalD.lean 1 declarations
ActualGlobalP.lean 1 declarations
ActualHemisphereInverse.lean 1 declarations
ActualInvariantTube.lean 5 declarations
ActualInverseMetric.lean 5 declarations
ActualLogCells.lean 1 declarations
ActualLogEnergy.lean 1 declarations
ActualLogGrowth.lean 3 declarations
ActualLogInequality.lean 1 declarations
ActualLogMeasure.lean 4 declarations
ActualLogMeasureEnergy.lean 1 declarations
ActualLogMeasureFurther.lean 19 declarations
ActualProductBounds.lean 2 declarations
ActualProjectiveAreaChart.lean 1 declarations
ActualProjectiveDensity.lean 1 declarations
ActualProjectiveInverse.lean 1 declarations
ActualRoundFEquation.lean 1 declarations
ActualSigmaInterpolation.lean 1 declarations
ActualSupportVariation.lean 1 declarations
ActualTubeArea.lean 3 declarations
ActualTubeEnergy.lean 1 declarations
ActualTubeMetricPositivity.lean 7 declarations
ActualTubeSecond.lean 3 declarations
ActualTubeWeights.lean 6 declarations
ActualWeightedAngular.lean 2 declarations
ActualWeightedAngularFurther.lean 1 declarations
ActualWeightedBase.lean 2 declarations
ActualWeightedG.lean 1 declarations
ActualWeightedLog.lean 1 declarations
AffineBoxArea.lean 4 declarations
AffineCapArea.lean 1 declarations
AffineCapGeometry.lean 6 declarations
AffineCapLIntegral.lean 1 declarations
AffineFamily.lean 20 declarations
AffineGaussSurjectivity.lean 1 declarations
AffineImageCoordinates.lean 3 declarations
AffineInvariantCap.lean 6 declarations
AffineParametricStationarity.lean 3 declarations
AffineStripArea.lean 4 declarations
AffineSupport.lean 13 declarations
AmbientImmersion.lean 2 declarations
AmbientStraightening.lean 9 declarations
AngularCalculus.lean 13 declarations
AngularCofactor.lean 4 declarations
BaseConcavity.lean 1 declarations
BaseExponentialIBP.lean 4 declarations
BaseLogIdentity.lean 4 declarations
BaseWeightedIBP.lean 5 declarations
BaseWeightedIntegral.lean 3 declarations
Basic.lean 11 declarations
BilinearNewton.lean 19 declarations
BlockNewton.lean 3 declarations
BoundedHarmonic.lean 3 declarations
CapArea.lean 5 declarations
CapChangeOfVariables.lean 6 declarations
CapCoordinates.lean 17 declarations
CapCovariance.lean 9 declarations
CapGeometry.lean 5 declarations
CapInverseBound.lean 4 declarations
CapPerturbation.lean 3 declarations
CofactorCodazzi.lean 2 declarations
CompactDifferentiation.lean 1 declarations
CompactIntegration.lean 10 declarations
CompletePositiveCap.lean 8 declarations
CompletePositiveCapFurther.lean 3 declarations
CompleteSphericalCaps.lean 1 declarations
ConjugationNewton.lean 3 declarations
ConstantDet.lean 3 declarations
ConstantDetCalculus.lean 11 declarations
ConstantHessianQuadratic.lean 3 declarations
ConvexGradientBound.lean 10 declarations
ConvexLocalLimits.lean 13 declarations
ConvexSmoothMax.lean 10 declarations
DensityTransform.lean 4 declarations
DetBarrierBound.lean 2 declarations
DetBarrierPhase.lean 6 declarations
DetCompactBound.lean 3 declarations
DetInteriorBall.lean 1 declarations
DeterminantVariation.lean 44 declarations
DirectionalJacobi.lean 10 declarations
DualDetBarrier.lean 12 declarations
DualDetBound.lean 2 declarations
DualDetCompact.lean 4 declarations
DualDetPhase.lean 5 declarations
DualHeightCalculus.lean 13 declarations
EllipticComparison.lean 4 declarations
EntireAndDoubling.lean 12 declarations
EntireGlobalDet.lean 3 declarations
EntireGraphComplete.lean 2 declarations
EuclideanChain.lean 12 declarations
FaceSigmaTransport.lean 1 declarations
FiberArea.lean 1 declarations
FiniteAreaCover.lean 2 declarations
FiniteProjectiveCharts.lean 7 declarations
FixedBasisCoordinates.lean 5 declarations
FlatBlockCalculus.lean 6 declarations
FlatChartArea.lean 1 declarations
FlatChartInjective.lean 2 declarations
FlatEulerCore.lean 7 declarations
FlatFCalculus.lean 9 declarations
FlatFEquation.lean 3 declarations
FlatGraphCoverage.lean 1 declarations
FlatInverseMetric.lean 3 declarations
FlatLogCalculus.lean 5 declarations
FlatLogEuler.lean 8 declarations
FlatParametricArea.lean 1 declarations
FlatProductCoordinates.lean 11 declarations
FlatSupportImmersion.lean 2 declarations
FlatTestHessian.lean 4 declarations
FlatTubeArea.lean 6 declarations
FlatTubeChart.lean 3 declarations
FlatTubeEuler.lean 6 declarations
FlatTubePositive.lean 3 declarations
FlatWeightedEuler.lean 1 declarations
GaussCoordinates.lean 11 declarations
GaussSurjectivity.lean 2 declarations
GeneralCapCoordinates.lean 4 declarations
GeneralPositiveCap.lean 2 declarations
GlobalDetRatio.lean 2 declarations
GlobalFlatAreaLIntegral.lean 1 declarations
GlobalFlatInverseLIntegral.lean 1 declarations
GlobalGraphChart.lean 2 declarations
GlobalHessianBound.lean 4 declarations
GraphAreaCharts.lean 7 declarations
GraphBallArea.lean 5 declarations
GraphParametricArea.lean 12 declarations
GraphPatchArea.lean 5 declarations
HessianCompactness.lean 5 declarations
HessianDivergence.lean 4 declarations
HessianDominance.lean 2 declarations
HessianMinors.lean 2 declarations
HessianTraceIntegral.lean 3 declarations
HessianVariation.lean 8 declarations
HomogeneousSphere.lean 1 declarations
ImmersionStationary.lean 2 declarations
IntegratedParametricStationarity.lean 4 declarations
InteriorLimits.lean 16 declarations
InverseTracePullback.lean 5 declarations
JetCalculus.lean 4 declarations
JointAngularCalculus.lean 13 declarations
JointTubeMetrics.lean 12 declarations
LinearLogTrace.lean 4 declarations
LinearNormalizationCalculus.lean 12 declarations
LinearSphere.lean 2 declarations
LinearizedNormalization.lean 5 declarations
LocalAreaStationarity.lean 1 declarations
LocalDet.lean 1 declarations
LocalMaximumHessian.lean 5 declarations
LocalMaximumSecond.lean 1 declarations
LocalVelocity.lean 4 declarations
LogBarrierCalculus.lean 12 declarations
LogCaccioppoli.lean 8 declarations
LogCellBound.lean 3 declarations
LogDetGradientEnergy.lean 5 declarations
LogMassWeight.lean 2 declarations
LogTubeMeasure.lean 8 declarations
LogVariance.lean 5 declarations
Main.lean 1 declarations
MassIntegral.lean 2 declarations
MassInterpolation.lean 3 declarations
MassUpper.lean 1 declarations
MatrixCombination.lean 2 declarations
MatrixConcavity.lean 26 declarations
MatrixDetRigidity.lean 2 declarations
MatrixMetric.lean 9 declarations
MatrixShiftBound.lean 3 declarations
MatrixShiftDet.lean 2 declarations
MatrixUniformBounds.lean 2 declarations
MaximalModelExclusion.lean 4 declarations
ModelCentering.lean 18 declarations
ModelCenteringFurther.lean 41 declarations
ModelFaceMass.lean 1 declarations
ModelLimit.lean 8 declarations
ModelPositiveLogMass.lean 2 declarations
ModelPositiveSigma.lean 3 declarations
NewtonBasis.lean 18 declarations
NewtonBasisFurther.lean 5 declarations
NewtonField.lean 2 declarations
NewtonPiola.lean 4 declarations
NewtonTensor.lean 4 declarations
NoNormalizedMaximalModel.lean 1 declarations
NoOrthant.lean 3 declarations
NoZeroTransverse.lean 4 declarations
NormalizedCaps.lean 11 declarations
NormalizedCellGeometry.lean 11 declarations
NormalizedCriticalDensity.lean 1 declarations
NormalizedDet.lean 2 declarations
NormalizedDetLower.lean 2 declarations
NormalizedFamilyDet.lean 2 declarations
NormalizedHessianUpper.lean 4 declarations
NormalizedLogVariance.lean 4 declarations
NormalizedSigma.lean 1 declarations
NormalizedSigmaTransport.lean 2 declarations
NormedCompactInterior.lean 6 declarations
NormedInteriorLimits.lean 2 declarations
OrthantGeometry.lean 7 declarations
OrthantHeight.lean 8 declarations
ParametricAffineArea.lean 7 declarations
ParametricBasis.lean 2 declarations
ParametricChangeOfCoordinates.lean 6 declarations
ParametricChartStationarity.lean 1 declarations
ParametricChoiceTransport.lean 2 declarations
ParametricChoices.lean 5 declarations
ParametricDensityCoordinates.lean 1 declarations
ParametricFirstVariation.lean 3 declarations
ParametricGraphJets.lean 10 declarations
ParametricInverseMetric.lean 6 declarations
ParametricNormalization.lean 5 declarations
ParametricSmoothness.lean 9 declarations
ParametricStationarity.lean 2 declarations
ParametricTransport.lean 8 declarations
ParametricVariationAlgebra.lean 11 declarations
PiolaAlgebra.lean 6 declarations
PiolaDifferential.lean 3 declarations
PositiveDerivative.lean 7 declarations
PositiveFaceLimit.lean 2 declarations
PositiveFaceMass.lean 2 declarations
PositiveLimitCap.lean 1 declarations
PositiveMassAlgebra.lean 3 declarations
PositiveMatrixTraceBound.lean 13 declarations
ProductAmbientCoordinates.lean 5 declarations
ProductAreaChart.lean 1 declarations
ProductEquator.lean 4 declarations
ProjectiveCone.lean 2 declarations
ProjectiveDensity.lean 2 declarations
ProjectiveEnergyContinuity.lean 2 declarations
ProjectiveHemisphere.lean 2 declarations
ProjectiveInverseWeight.lean 3 declarations
ProjectiveNormalized.lean 2 declarations
ProjectiveWeightContinuity.lean 6 declarations
QuadraticAffineImage.lean 3 declarations
QuadraticIntegration.lean 1 declarations
RadialAdjugate.lean 10 declarations
RadialAdjugateGL.lean 3 declarations
RegularFiberDomain.lean 8 declarations
RoundCofactorInverse.lean 2 declarations
RoundContractions.lean 7 declarations
RoundSliceContractions.lean 5 declarations
SectionNormalizationFamily.lean 1 declarations
SegmentEnergy.lean 4 declarations
SigmaBaseTransport.lean 3 declarations
SigmaCapHelpers.lean 5 declarations
SigmaNormalization.lean 5 declarations
SigmaTransform.lean 2 declarations
SimultaneousMinima.lean 2 declarations
SmoothCapTest.lean 9 declarations
SmoothCoefficients.lean 5 declarations
SmoothGraphChart.lean 3 declarations
SmoothParameter.lean 4 declarations
SmoothPositivePart.lean 15 declarations
SphereAlgebra.lean 6 declarations
SphereDivergence.lean 9 declarations
SphereIntegration.lean 18 declarations
SphereIsometry.lean 4 declarations
SphereTensorCalculus.lean 5 declarations
SphericalAreaContinuity.lean 2 declarations
SupersolutionHighSet.lean 1 declarations
SupportAnnulus.lean 3 declarations
SupportArea.lean 4 declarations
SupportCoordinates.lean 12 declarations
SupportGeometry.lean 18 declarations
SupportHomogeneity.lean 5 declarations
SupportOrientation.lean 2 declarations
SupportRadial.lean 5 declarations
SupportVariation.lean 15 declarations
SupportVariationJets.lean 6 declarations
TangentShiftCalculus.lean 9 declarations
TargetCapLIntegral.lean 3 declarations
TensorFlux.lean 14 declarations
TensorIntegration.lean 3 declarations
ThinSlices.lean 16 declarations
TiltedLIntegral.lean 2 declarations
TiltedTrace.lean 5 declarations
TracefreeMatrix.lean 2 declarations
TranslateDet.lean 5 declarations
TriangularGraph.lean 8 declarations
TubeChartConstruction.lean 3 declarations
TubeCombination.lean 20 declarations
TubeCompactIntegral.lean 19 declarations
TubeDensity.lean 4 declarations
TubeDensityIntegralCompact.lean 1 declarations
TubeDensityVariation.lean 8 declarations
TubeFrame.lean 8 declarations
TubeInvariantSmooth.lean 6 declarations
TubeLinearTransform.lean 3 declarations
TubeMetricPositivity.lean 6 declarations
TubeSecondForm.lean 8 declarations
TubeSumIntegral.lean 2 declarations
TubeSupportedIntegral.lean 3 declarations
TubeWeightAlgebra.lean 4 declarations
UniformActualCells.lean 3 declarations
UniformFlatCap.lean 1 declarations
UniformLogCells.lean 6 declarations
UniformProductCap.lean 1 declarations
UniformSigmaCaps.lean 1 declarations
UniformSphericalCap.lean 20 declarations
VarianceSeparation.lean 2 declarations
WeightTransform.lean 4 declarations
WeightedCapInverse.lean 1 declarations
WeightedChartArea.lean 1 declarations
WeightedChartLIntegral.lean 1 declarations
WeightedDivergence.lean 6 declarations
WeightedLogEnergy.lean 1 declarations
WeightedMassUpper.lean 2 declarations
WeightedPoincare.lean 5 declarations
WeightedTracefreeMatrix.lean 2 declarations
WeightedTubeEnergy.lean 1 declarations
WholeGraphAreaTransport.lean 1 declarations
WholeSphereInverse.lean 1 declarations
WholeSphereProjective.lean 2 declarations