`OAI/Analysis/Mahler/`

2056 declarations, 0 contain sorry, 0 declared as axioms; 243 files

Files

ActualFiniteStrips.lean 11 declarations
ActualVerticalPrimitive.lean 12 declarations
AngularEndpoint.lean 5 declarations
AngularFibers.lean 8 declarations
AngularGeometry.lean 32 declarations
AngularIntegrals.lean 7 declarations
AngularStrip.lean 10 declarations
BasisContinuousWedge.lean 5 declarations
BoundaryJet.lean 13 declarations
ChartExtension.lean 7 declarations
ChartStokes.lean 6 declarations
Classification.lean 40 declarations
ClosedBoundaryStokes.lean 3 declarations
ClosedWedgePowers.lean 9 declarations
CompactFluxDifferentiation.lean 5 declarations
CompactIntegral.lean 8 declarations
ComplexCoordinates.lean 11 declarations
ComplexSphereIntegral.lean 6 declarations
ComplexStripMap.lean 20 declarations
ComplexVolume.lean 8 declarations
ConformalInjectivity.lean 8 declarations
ConformalInverse.lean 17 declarations
ConformalRadialRegularity.lean 7 declarations
ConformalSeries.lean 36 declarations
ContinuousWedge.lean 9 declarations
ContinuousWedgeDerivative.lean 4 declarations
ConvexApproximation.lean 8 declarations
ConvexCompletion.lean 6 declarations
ConvexENNRealTransfer.lean 1 declarations
ConvexGeometry.lean 14 declarations
ConvexMain.lean 2 declarations
ConvexMassReduction.lean 1 declarations
ConvexPolarBody.lean 4 declarations
ConvexSequence.lean 7 declarations
ConvexTransfer.lean 2 declarations
CoordinateAnnulus.lean 8 declarations
CoordinateBall.lean 12 declarations
CoordinateEuclidean.lean 3 declarations
CoordinateSphere.lean 3 declarations
CovectorVolume.lean 7 declarations
DCForms.lean 9 declarations
DCRegularity.lean 2 declarations
Diamonds.lean 27 declarations
DilationTransport.lean 8 declarations
DimensionTwoAssembly.lean 4 declarations
EqualityMedians.lean 29 declarations
ErrorBound.lean 16 declarations
EuclideanMassDensity.lean 3 declarations
EuclideanRegularLevels.lean 4 declarations
EuclideanSpecialMap.lean 8 declarations
ExactFormCoordinates.lean 10 declarations
ExactSphereFluxBridge.lean 3 declarations
ExactSphereStokes.lean 3 declarations
ExteriorAlternatization.lean 10 declarations
ExteriorCoefficient.lean 1 declarations
ExteriorCoordinates.lean 6 declarations
ExteriorDirectional.lean 1 declarations
ExteriorFlux.lean 18 declarations
ExteriorHessian.lean 3 declarations
ExteriorLeibnizTwo.lean 6 declarations
ExteriorPower.lean 10 declarations
Faces.lean 92 declarations
FiberEndpoint.lean 6 declarations
FiberHeight.lean 6 declarations
FiberPreimageEndpoint.lean 2 declarations
FiberPrimitive.lean 6 declarations
FiniteStripReduction.lean 3 declarations
FiniteStrips.lean 13 declarations
FluxVariation.lean 5 declarations
FormLocalization.lean 6 declarations
FormStokes.lean 3 declarations
GlobalFiberParametrization.lean 8 declarations
GlobalPlanarBound.lean 4 declarations
GlobalPlanarMonotonicity.lean 1 declarations
GlobalVerticalGeometry.lean 13 declarations
HalfspaceStokes.lean 9 declarations
HannerBodies.lean 90 declarations
HemisphereArea.lean 12 declarations
HemisphereChart.lean 20 declarations
HemisphereFlux.lean 7 declarations
HemisphereJacobian.lean 7 declarations
HemisphereMeasure.lean 8 declarations
Hessian.lean 30 declarations
HolomorphicLogC2.lean 5 declarations
HolomorphicRegularity.lean 4 declarations
HomogeneousCircleIntegral.lean 5 declarations
HomogeneousDeformation.lean 8 declarations
HomogeneousDensityVariation.lean 3 declarations
HomogeneousEndpoint.lean 4 declarations
HomogeneousFlux.lean 12 declarations
HomogeneousFluxDifferentiation.lean 10 declarations
HomogeneousFluxFTC.lean 3 declarations
HomogeneousMassAssembly.lean 2 declarations
HomogeneousPrimitiveRegularity.lean 8 declarations
HomogeneousSmoothForms.lean 5 declarations
HomogeneousSphereIntegral.lean 7 declarations
HomogeneousTransgression.lean 7 declarations
HomogeneousTransgressionFTC.lean 4 declarations
HomogeneousTwoFlux.lean 6 declarations
HomogeneousTwoTransgression.lean 6 declarations
HomogeneousVariationCoefficient.lean 3 declarations
HorizontalForms.lean 11 declarations
ImplicitAngle.lean 4 declarations
InteriorStokes.lean 5 declarations
InverseRadialRegularity.lean 5 declarations
Jacobian.lean 11 declarations
Lens.lean 62 declarations
LevelFace.lean 14 declarations
LevelForms.lean 3 declarations
LogDilation.lean 7 declarations
LogJet.lean 8 declarations
LogNormSquare.lean 5 declarations
LogScalarJet.lean 5 declarations
LogUniform.lean 4 declarations
LowDimensionalBodies.lean 2 declarations
MainTheorem.lean 1 declarations
MassLimit.lean 4 declarations
MassTarget.lean 5 declarations
MatrixExteriorPower.lean 14 declarations
MatrixHessian.lean 23 declarations
Medians.lean 44 declarations
NormExteriorPower.lean 11 declarations
NormSquareForm.lean 5 declarations
NormSquareJet.lean 9 declarations
OpenExteriorNormalization.lean 9 declarations
OpenHessian.lean 11 declarations
OrientedChartIntegral.lean 6 declarations
OrientedSphereDensity.lean 13 declarations
PairExteriorBridge.lean 1 declarations
PairTransgression.lean 8 declarations
PlanarDensity.lean 13 declarations
PlanarErrorRate.lean 4 declarations
PlanarEstimates.lean 8 declarations
PlanarIntegralRegularity.lean 9 declarations
PlanarRegularity.lean 12 declarations
PlanarSymmetry.lean 3 declarations
Positivity.lean 12 declarations
PowerTransgression.lean 6 declarations
PrimitiveBound.lean 8 declarations
PrimitiveEquality.lean 2 declarations
PrimitiveRegularity.lean 7 declarations
PullbackRegularity.lean 3 declarations
PunctureCutoff.lean 8 declarations
PuncturedBallStokes.lean 5 declarations
PuncturedSublevelStokes.lean 2 declarations
RadialBridge.lean 12 declarations
RadialPrimitiveDeriv.lean 5 declarations
RadiusSphereIntegral.lean 2 declarations
RawAlternatingCalculus.lean 2 declarations
RawAlternationDerivative.lean 4 declarations
RawClosedPower.lean 4 declarations
RawClosedProduct.lean 9 declarations
RawCoefficientDerivative.lean 5 declarations
RawExteriorPower.lean 10 declarations
RawReindexedDerivative.lean 7 declarations
RealLogBridge.lean 7 declarations
ReferencePole.lean 10 declarations
ReferencePoleFrame.lean 11 declarations
ReferenceSphere.lean 7 declarations
ReferenceSphereIntegral.lean 6 declarations
RegularBoundaryAtlas.lean 6 declarations
RegularChartStokes.lean 6 declarations
RegularLevelCharts.lean 9 declarations
RegularMassReduction.lean 2 declarations
RegularPartition.lean 5 declarations
RegularStokesAssembly.lean 1 declarations
RegularSublevel.lean 5 declarations
RescaledHolomorphic.lean 3 declarations
RescaledMassMap.lean 10 declarations
RescalingEstimates.lean 3 declarations
ShellRegularity.lean 10 declarations
SineBound.lean 5 declarations
SmallSphereLimits.lean 4 declarations
SourceBoundaryIntegral.lean 2 declarations
SourceCanonicalMeasure.lean 5 declarations
SourceCoordinateExterior.lean 3 declarations
SourceCoordinateForms.lean 11 declarations
SourceCoordinateMeasure.lean 1 import, no declarations
SourceExteriorDerivative.lean 7 declarations
SourceFluxCoordinates.lean 8 declarations
SourceFluxRegularity.lean 12 declarations
SourceFullExterior.lean 4 declarations
SourceHomogeneous.lean 6 declarations
SourceLevelFlux.lean 9 declarations
SourceLogC2.lean 6 declarations
SourcePrimitiveStokes.lean 3 declarations
SourceRadiusFlux.lean 5 declarations
SourceRawCoefficient.lean 4 declarations
SourceRawJets.lean 7 declarations
SourceRawOrientation.lean 4 declarations
SourceRealExterior.lean 2 declarations
SourceRegularFlux.lean 1 declarations
SourceRegularLimit.lean 2 declarations
SourceRegularMass.lean 2 declarations
SourceRescaling.lean 2 declarations
SourceSphereLimit.lean 7 declarations
SourceStokes.lean 6 declarations
SourceTopCoordinates.lean 5 declarations
SpecialJacobian.lean 7 declarations
SpecialLeadingTerm.lean 12 declarations
SpecialMassBridge.lean 7 declarations
SpecialMassHypotheses.lean 4 declarations
SpecialSourceMass.lean 3 declarations
SphereAreaTransport.lean 7 declarations
SphereCoordinateIntegral.lean 4 declarations
SphereDensityBridge.lean 15 declarations
SphereDensityRestriction.lean 3 declarations
SphereFlux.lean 11 declarations
SphereFluxDifferentiation.lean 6 declarations
SphereFluxIntegral.lean 10 declarations
SphereFluxLimit.lean 4 declarations
SphereForms.lean 13 declarations
SphereNormalization.lean 3 declarations
SphereOrientation.lean 8 declarations
SphereRadius.lean 5 declarations
SphereTransport.lean 5 declarations
SphereVolumeOrientation.lean 2 declarations
Splitting.lean 49 declarations
StripCompactSublevels.lean 6 declarations
StripDifferential.lean 8 declarations
StripGeometry.lean 4 declarations
StripJacobian.lean 4 declarations
StripLevelGeometry.lean 2 declarations
StripMassExhaustion.lean 8 declarations
StripRankGeometry.lean 11 declarations
StripRegularLevels.lean 2 declarations
StripRegularValues.lean 7 declarations
StripSublevelTopology.lean 7 declarations
StripVolume.lean 8 declarations
TailIntegral.lean 13 declarations
UniformError.lean 7 declarations
UniformJet.lean 2 declarations
UnitaryReference.lean 6 declarations
VerticalRadius.lean 8 declarations
VerticalSpeed.lean 6 declarations
WedgeAlgebra.lean 5 declarations
WedgeAssociativity.lean 4 declarations
WedgeCalculus.lean 4 declarations
WedgeDecomposition.lean 6 declarations
WedgeEven.lean 7 declarations
WedgeOne.lean 5 declarations
WedgeTwoDifferentialAlgebra.lean 7 declarations
WedgeUnit.lean 7 declarations