`OAI/Analysis/SymmetricDomains/`

2179 declarations, 0 contain sorry, 0 declared as axioms; 351 files

Files

ActionAutomorphismHomRange.lean 9 declarations
AdNilpotentPositiveDilations.lean 13 declarations
AffineBand.lean 11 declarations
AffineInverseGermSemialgebraic.lean 6 declarations
AffineProductCoordinates.lean 5 declarations
AlgebraicBranchRamification.lean 12 declarations
AlgebraicGraphPolynomial.lean 3 declarations
AlgebraicIndependentNashPartials.lean 9 declarations
AmbientInverse.lean 10 declarations
AnalyticDirectionalDerivationFun.lean 8 declarations
AnalyticExtensionSemialgebraicAlgebraic.lean 2 declarations
AnalyticFamilyRegraph.lean 1 declarations
AnalyticGermMatrixRank.lean 3 declarations
AnalyticImplicitScalar.lean 10 declarations
AnalyticMulZeroGerm.lean 9 declarations
AnalyticNashRank.lean 8 declarations
AnalyticNashRefinement.lean 8 declarations
AnalyticNhdDifferentiableAffine.lean 35 declarations
AnalyticReparameterization.lean 3 declarations
AnalyticSecondJetCoordinates.lean 12 declarations
AnalyticZeroNull.lean 11 declarations
AnalyticZeroRealPolydisc.lean 2 declarations
AutChartConjugationJacobian.lean 1 declarations
AutChartUnimodularJacobian.lean 2 declarations
AutFirstJetRegular.lean 2 declarations
Basic.lean 20 declarations
BiHaarInvInvariant.lean 2 declarations
BishopAnalyticDiscs.lean 15 declarations
BishopBoundarySolution.lean 13 declarations
BishopBoundarySolutionConstants.lean 2 declarations
BishopDiscRadialExpansion.lean 5 declarations
BishopNormalZeroDeformation.lean 5 declarations
BishopPathInterior.lean 10 declarations
BishopPositiveInterior.lean 1 declarations
BishopTransverseNoncollapse.lean 5 declarations
BoundaryFiberClosureContinuity.lean 7 declarations
BoundaryInjective.lean 123 declarations
BoundaryParameterPeakMaximizer.lean 4 declarations
BoundaryParametricDimensionLt.lean 1 declarations
C1PerturbedFamilyLocal.lean 4 declarations
CartanUniqueness.lean 2 declarations
CayleyTangentBound.lean 16 declarations
Centered.lean 7 declarations
CenteredChartGerms.lean 1 declarations
ChartAbsDetOne.lean 2 declarations
ChartDensityMeasureLeft.lean 10 declarations
ChartDensityPreservedBy.lean 4 declarations
ChartDimensionLeCoordinate.lean 5 declarations
ChartJacobianNeZero.lean 2 declarations
ChartLeftDensityJacobian.lean 4 declarations
ChartLimitMapsAnchor.lean 1 declarations
ChoosePositiveC1Regularization.lean 4 declarations
ClosedMaximizerRelation.lean 5 declarations
CocompactAffinePointOr.lean 3 declarations
CocompactChartDiscContinuity.lean 4 declarations
CocompactScaling.lean 1 declarations
CommutingGeneratorsValueZero.lean 3 declarations
CompactFaithfulIsotropy.lean 16 declarations
CompactPeakRatio.lean 11 declarations
CompactSupportRates.lean 2 declarations
CompleteGeneratorJetProjection.lean 2 declarations
CompleteGeneratorLieAlgebra.lean 4 declarations
CompleteGeneratorTraceAd.lean 2 declarations
ComplexNashNormalGraph.lean 1 declarations
ComplexTangentRankAlternative.lean 5 declarations
ComplexTensorNormalForm.lean 4 declarations
ComplexificationRankLeReal.lean 3 declarations
ComplexifyRealContinuousEquiv.lean 9 declarations
ConjugateMulActionCompact.lean 4 declarations
ConsistentIteratesTendsto.lean 2 declarations
ConsistentVariableStepsTendsto.lean 3 declarations
ContinuityPrinciple.lean 13 declarations
ContinuousAutTransport.lean 11 declarations
ContinuousFderivLocallyUniform.lean 6 declarations
CoordinateDerivativeRank.lean 6 declarations
CoordinateFieldApply.lean 12 declarations
CoordinateFieldLinear.lean 4 declarations
CosineBumpWeightedSummable.lean 8 declarations
CriticalAffineBundleNeighborhood.lean 8 declarations
CriticalCountableCharts.lean 6 declarations
CurvePowerDisplacement.lean 3 declarations
CurveUniformConsistency.lean 2 declarations
Cutoff.lean 3 declarations
DecayWeightDeriv.lean 8 declarations
DifferentiableCauchyTransform.lean 7 declarations
DifferentialMemSpanTranscendence.lean 3 declarations
DiscCompactness.lean 12 declarations
DiscRelationCompactLocal.lean 18 declarations
DisplacementBoundByFirst.lean 2 declarations
DivisibleAutomorphismsSubsequence.lean 1 declarations
DivisibleBochnerCoordinate.lean 17 declarations
DivisibleHermitianModel.lean 2 declarations
EntireSupports.lean 1 declarations
EtaleDerivationExtensionUnique.lean 6 declarations
EulerSpectrum.lean 20 declarations
EventualEquicontinuityOpenSubset.lean 3 declarations
EventualOffsetBall.lean 15 declarations
EventuallyImageBallNonzero.lean 9 declarations
ExpandingBiholomorphismsCharts.lean 2 declarations
FiberCardAmbientSheets.lean 10 declarations
FiberPolynomialNatDegree.lean 10 declarations
FieldSecondJet.lean 27 declarations
FiniteAlgebraGenericSheets.lean 7 declarations
FiniteCommonRamification.lean 3 declarations
FiniteCoveringRamifiedSection.lean 18 declarations
FiniteDimensionalCompleteGenerator.lean 11 declarations
FiniteFlowParametrization.lean 2 declarations
FiniteNashCoverAffine.lean 2 declarations
FiniteNashCoverVertical.lean 2 declarations
FiniteProperMapOpen.lean 14 declarations
FiniteUnion.lean 17 declarations
FirstJetConstMul.lean 2 declarations
FirstJetConstMul2.lean 3 declarations
FirstJetFlowMul.lean 2 declarations
FlatWeightedEuler.lean 5 declarations
FlowWordFirstJet.lean 6 declarations
ForwardBackwardGerm.lean 14 declarations
ForwardLocalDataCompact.lean 4 declarations
GeneratorAdjointContinuous.lean 4 declarations
GeneratorAdjointHom.lean 4 declarations
GeneratorDeterminantDerivZero.lean 11 declarations
GeneratorLieAdjoint.lean 2 declarations
GeneratorPushForwardLinear.lean 7 declarations
GenericAlgebraicBranchRamification.lean 1 declarations
GenericAlgebraicBranchRamification2.lean 2 declarations
GenericAlgebraicRamificationUniform.lean 2 declarations
GenericFinParameterPolynomial.lean 6 declarations
GenericNashNormalCoordinates.lean 2 declarations
GenericNormalGraphProjection.lean 3 declarations
GenericPolynomialParameterFactor.lean 4 declarations
GenericRealParameterPolynomial.lean 5 declarations
GenericSupportedBoundary.lean 1 declarations
GenericSurjectiveRealNormal.lean 6 declarations
GenericTangentComplexNormal.lean 6 declarations
Geometry.lean 5 declarations
Geometry2.lean 4 declarations
Geometry3.lean 2 declarations
GlobalQuadraticScaling.lean 1 declarations
GlobalTwoSided.lean 2 declarations
GoodNashBoundary.lean 8 declarations
GoodSupportedBoundary.lean 2 declarations
GraphBoundaryFirstHomotopy.lean 3 declarations
HeisenbergShiftAxis.lean 10 declarations
HermPartUnit.lean 33 declarations
HermiteSignature.lean 10 declarations
HermitianModelSymmetric.lean 2 declarations
HolQuadraticSmul.lean 13 declarations
HolomorphicIdSmallIterates.lean 3 declarations
HolomorphicLocallyUniformLimit.lean 7 declarations
HolomorphicNearIdLower.lean 2 declarations
HolomorphicSupportIndependent.lean 3 declarations
HomeomorphInverse.lean 3 declarations
HorizontalGraphComplexification.lean 7 declarations
HurwitzZeroFreeOr.lean 3 declarations
ImagPartLieReal.lean 23 declarations
IndependentChartConormals.lean 3 declarations
IndependentComplexConormalRows.lean 4 declarations
IndependentConormals.lean 9 declarations
IndependentSupportCoercivity.lean 2 declarations
IndependentSupportRows.lean 3 declarations
InfinitesimalGeneratorEquivariant.lean 6 declarations
InjectiveConormalFinrank.lean 3 declarations
InnerExp.lean 14 declarations
IntegralPrimitive.lean 8 declarations
InteriorBallsAnalyticGraphs.lean 4 declarations
InteriorBallsChangeCoordinates.lean 1 declarations
InteriorBallsSmallSlope.lean 1 declarations
InteriorBallsTotallyReal.lean 1 declarations
InterpolateRealUpper.lean 11 declarations
InverseChartGaussian.lean 5 declarations
InvolutionDerivativeNegId.lean 3 declarations
IsotropyCentralShiftZero.lean 2 declarations
IsotropyCompleteGeneratorsTotally.lean 2 declarations
IsotropyRepresentationUnitsCompact.lean 11 declarations
IterateAverageCoboundary.lean 6 declarations
JointLimitRamification.lean 4 declarations
JointZeroConeProper.lean 3 declarations
LieBracketIndicatorConst.lean 6 declarations
Local.lean 2 declarations
LocalAutomorphismODEGroup.lean 2 declarations
LocalAutomorphismODEGroup2.lean 1 declarations
LocalBishopData.lean 2 declarations
LocalHaarEqualMass.lean 2 declarations
LocalInverseSupportScaled.lean 2 declarations
LocalMaxGraphParameter.lean 9 declarations
LocalRealHomExtension.lean 3 declarations
LocallyGoodNashBoundary.lean 2 declarations
LocallySmallSlopeGood.lean 5 declarations
LogarithmicPeakBound.lean 6 declarations
Main.lean 1 declarations
MaximizerBundleBorel.lean 9 declarations
MeromorphicGermDetZero.lean 2 declarations
MeromorphicPolynomialRoot.lean 2 declarations
MeromorphicRemovablePositiveRay.lean 2 declarations
Model.lean 9 declarations
ModelAxisNegativeIsotropy.lean 4 declarations
ModelChartOpen.lean 8 declarations
ModelComplexField.lean 7 declarations
ModelIsotropyCentralShift.lean 3 declarations
ModelNormalTranslationAd.lean 9 declarations
ModelRotationWeight.lean 11 declarations
ModelUnaveraged.lean 3 declarations
MontelExpandingDomains.lean 7 declarations
NashCellGeometricRank.lean 2 declarations
NashCellIntrinsicRank.lean 2 declarations
NashCellLowRank.lean 1 declarations
NashNormalGraphBoundary.lean 5 declarations
NashParametrizationExtension.lean 4 declarations
NoncollapseC1Scaling.lean 3 declarations
NoncollapsedSupportedBoundary.lean 3 declarations
NormalOffsetFamilyJoint.lean 9 declarations
NormalOffsetNoncollapse.lean 4 declarations
NormalScaleBound.lean 4 declarations
NormalizedAutomorphismLimitComplete.lean 1 declarations
NormalizedAutomorphismLocalLimit.lean 1 declarations
NormalizedAutomorphismsHaveNonzero.lean 2 declarations
NormalizedDisplacementZeroUniform.lean 3 declarations
NormalizedLocalInverse.lean 8 declarations
OffsetDerivative.lean 6 declarations
OffsetLimitClosedCone.lean 5 declarations
OldOffsetOldPosition.lean 12 declarations
OneKernel.lean 17 declarations
OneParameterDerivativeJoint.lean 3 declarations
OneParameterDifferentiableZero.lean 11 declarations
OneParameterFderivDeriv.lean 3 declarations
OneParameterGeneratorAdd.lean 2 declarations
OneParameterJointStrict.lean 3 declarations
OneParameterLocalODE.lean 3 declarations
OneParameterOneGenerator.lean 3 declarations
OneParameterPositiveLocal.lean 1 declarations
OneParameterPositiveLocal2.lean 1 declarations
OpenChartLeftTranslate.lean 2 declarations
OpenDimension.lean 4 declarations
Pair.lean 12 declarations
ParameterPeakMaximizer.lean 7 declarations
PointSymmetryNegId.lean 3 declarations
PolynomialEmptyInterior.lean 4 declarations
PolynomialIntegralCoordinates.lean 9 declarations
PolynomialRamifiedAnalyticRoot.lean 4 declarations
PolynomialRelationDependentPartials.lean 6 declarations
PolynomialRelationPropagates.lean 3 declarations
PolynomialRemovableLocal.lean 10 declarations
PolynomialRootFiberFinite.lean 5 declarations
PolynomialSignSetChoice.lean 2 declarations
PolynomialSignSetChoice2.lean 2 declarations
PolynomialSignSetFibre.lean 1 declarations
PolynomialSignSetFinite.lean 25 declarations
PolynomialSignSetFinite2.lean 5 declarations
PolynomialSignSetInf.lean 6 declarations
PolynomialSignSetOffset.lean 3 declarations
PolynomialSignSetProjection.lean 3 declarations
PolynomialSignSetProjection2.lean 4 declarations
PolynomialSignSetQuery.lean 11 declarations
PolynomialSignSetRoot.lean 21 declarations
PolynomialSignSetSigns.lean 3 declarations
PolynomialSignSetVector.lean 3 declarations
PositiveMaximizerFiber.lean 1 declarations
PositivePureDimension.lean 5 declarations
PositiveReal.lean 9 declarations
PositiveVertexJets.lean 9 declarations
PowersTendstoOneVanishing.lean 1 declarations
PrimeBoundaryGenericFiber.lean 2 declarations
PrimeZeroLocusFixed.lean 5 declarations
PrimeZeroLocusMaximum.lean 7 declarations
ProductCurveLocalAutomorphism.lean 3 declarations
ProductCurveLocalFlow.lean 3 declarations
ProjectedChartCommonCOne.lean 2 declarations
ProjectedChartConjugationDifferential.lean 2 declarations
ProjectedChartLeftDifferential.lean 1 declarations
ProjectedChartObservableCont.lean 3 declarations
ProjectedChartObservableStrict.lean 2 declarations
ProjectedJetSequencesNot.lean 3 declarations
ProjectionNashChartGerms.lean 4 declarations
ProjectionTangentGeneric.lean 3 declarations
ProperEventuallyFiberSubset.lean 16 declarations
PushForwardGeneratorDeriv.lean 1 declarations
QuadraticDomainConnectedComponent.lean 11 declarations
QuadraticModelDomain.lean 4 declarations
QuadraticModelResidualFiber.lean 10 declarations
RankOneModelSymmetric.lean 2 declarations
RatLieAlgebra.lean 3 declarations
RawQuadraticModelNormalization.lean 7 declarations
RealCriticalMatrix.lean 7 declarations
RealDirectionsTangent.lean 3 declarations
RealMeanPositive.lean 4 declarations
RealParameterPolarRemoval.lean 2 declarations
RealPolynomialAnalyticRoot.lean 6 declarations
RegularSimpleSheet.lean 3 declarations
RootEvaluationSurjective.lean 17 declarations
RootMomentCoefficients.lean 7 declarations
RootSignPattern.lean 5 declarations
SampleAllChambers.lean 3 declarations
ScalarConeImagePositive.lean 6 declarations
ScalarEquicontinuousHolomorphy.lean 11 declarations
ScalarModelSymmetric.lean 2 declarations
ScalarPointSymmetryMap.lean 15 declarations
ScalarTubeInvolution.lean 11 declarations
ScaledDiscC1Limit.lean 3 declarations
ScaledDiscDeltaC1.lean 4 declarations
ScaledLocal.lean 5 declarations
ScaledModelC1Limit.lean 9 declarations
ScaledRadialOperatorApply.lean 8 declarations
ScalingEmbeddedCharts.lean 1 declarations
ScalingExpanding.lean 2 declarations
ScalingOpenDomain.lean 2 declarations
SchwarzRadialExpansion.lean 6 declarations
SelectExcludedOffsets.lean 4 declarations
SemialgebraicAnalyticLocalInverse.lean 2 declarations
SemialgebraicBoundaryFiniteNash.lean 20 declarations
SemialgebraicChartBoundaryData.lean 5 declarations
SemialgebraicFiniteAnalyticNash.lean 2 declarations
SemialgebraicOffsetLimits.lean 5 declarations
SemialgebraicOffsetLimitsFamily.lean 8 declarations
SemialgebraicPolynomialNonzero.lean 6 declarations
SemialgebraicRamificationParametersComplex.lean 1 declarations
SemialgebraicSelectionAnalyticPath.lean 1 declarations
SignVariationsPositiveRoots.lean 9 declarations
SignatureRootValues.lean 10 declarations
SliceApproachingGraphs.lean 4 declarations
SliceGraphDerivativeBound.lean 17 declarations
SmallAutomorphismsHaveNonzero.lean 2 declarations
SmallSlopeGoodSupported.lean 2 declarations
SmallSlopeGraphComplexification.lean 5 declarations
SmoothFlatWeightedFourier.lean 4 declarations
SortedFiberSelection.lean 7 declarations
SquarefreeRelationOffDenominator.lean 2 declarations
StrictModelSupports.lean 4 declarations
SupportCayleyOpenImage.lean 9 declarations
SupportDifferentialsChangeChart.lean 2 declarations
SupportedHermitianModel.lean 1 declarations
SupportedHermitianWeightedModel.lean 1 declarations
SupportedPositiveFiberVarying.lean 2 declarations
SupportedWeightedLimit.lean 3 declarations
TarskiQueryCharpoly.lean 13 declarations
TendstoAmbientLocallyUniformly.lean 17 declarations
TransferSymmetries.lean 4 declarations
TransverseCutoffs.lean 10 declarations
UniformCurveTaylor.lean 3 declarations
UniformLatticeHaarRight.lean 3 declarations
UniformSmallOperators.lean 6 declarations
VanishingIdealPrime.lean 2 declarations
VariableEulerAutomorphismFamily.lean 3 declarations
Vector.lean 15 declarations
VectorLift.lean 14 declarations
VerticalPieceBasePolynomial.lean 9 declarations
WeightedChartTwoSided.lean 4 declarations
WeightedSquaredChartLimit.lean 5 declarations
WeightedTaylorUniformlyCompact.lean 11 declarations
WeightedUnscaleC1Error.lean 9 declarations
ZeroISmul.lean 3 declarations
ZeroLocusPolynomialSmooth.lean 11 declarations