OAI/Geometry/PrescribedRicci/
962 declarations, 0 contain sorry, 0 declared as axioms; 161 files
Files
- ArrayWirtinger.lean 9 declarations
- BoundedSmoothPoisson.lean 1 declarations
- CalabiBochner.lean 4 declarations
- CalabiCutoffCalculus.lean 8 declarations
- CalabiCutoffDifferential.lean 3 declarations
- CalabiGradient.lean 3 declarations
- CalabiLocalMaximum.lean 3 declarations
- CalabiLower.lean 5 declarations
- CalabiMetricC1.lean 5 declarations
- CalabiRough.lean 10 declarations
- CalabiTensorAlgebra.lean 13 declarations
- CalabiTensorBounds.lean 7 declarations
- CalabiTensorMetric.lean 14 declarations
- CalabiTrace.lean 7 declarations
- CalabiTraceBound.lean 6 declarations
- ChartSobolevAlgebra.lean 8 declarations
- ChernBianchi.lean 5 declarations
- ChernBochner.lean 2 declarations
- ChernConnection.lean 10 declarations
- ChernLuAlgebra.lean 6 declarations
- ChernLuConnection.lean 7 declarations
- ChernLuDifferential.lean 7 declarations
- ChernLuGradient.lean 4 declarations
- ChernPairDifferential.lean 11 declarations
- ChernRough.lean 3 declarations
- CofactorBilin.lean 5 declarations
- CofactorCore.lean 9 declarations
- CofactorCoreEquation.lean 1 declarations
- CofactorLocalization.lean 7 declarations
- CofactorWeakEquation.lean 12 declarations
- CompactParameterIntegral.lean 1 declarations
- CompactPathBounds.lean 1 declarations
- CompactPathRicci.lean 4 declarations
- ComplexIntegrationByParts.lean 14 declarations
- ComplexJet.lean 12 declarations
- ComplexJetProduct.lean 4 declarations
- ContractedBochner.lean 3 declarations
- CoordinateVolumeComparison.lean 8 declarations
- CurvatureCompactBounds.lean 8 declarations
- CurvatureRicci.lean 6 declarations
- CutoffJetBound.lean 2 declarations
- DeterminantJet.lean 8 declarations
- DimensionOnePotential.lean 4 declarations
- DimensionZeroPotential.lean 2 declarations
- DirectionalInterpolation.lean 1 declarations
- DiscreteInterpolation.lean 4 declarations
- DiscreteManyProduct.lean 3 declarations
- FamilyJetNorm.lean 7 declarations
- FiniteCofactor.lean 9 declarations
- FiniteCofactorPatch.lean 10 declarations
- FixedCofactorBootstrap.lean 7 declarations
- FixedCofactorStep.lean 3 declarations
- GlobalKahlerEnergy.lean 9 declarations
- GlobalKahlerIntegral.lean 17 declarations
- GlobalSmoothCompact.lean 4 declarations
- HermitianCoercivity.lean 5 declarations
- HermitianPair.lean 12 declarations
- HermitianTensorEnergy.lean 10 declarations
- HolderFiniteProduct.lean 2 declarations
- IntegratedKahlerEnergy.lean 4 declarations
- InterpolationExponents.lean 8 declarations
- JetInterpolation.lean 8 declarations
- JetPolynomial.lean 13 declarations
- JetProductL2.lean 1 declarations
- JetRemainder.lean 13 declarations
- JetRemainderBound.lean 3 declarations
- JetSobolev.lean 9 declarations
- JetTameProduct.lean 2 declarations
- JetTrim.lean 12 declarations
- KaehlerLogTrace.lean 5 declarations
- KaehlerTrace.lean 9 declarations
- KahlerCauchySchwarz.lean 7 declarations
- KahlerChartGradient.lean 5 declarations
- KahlerChartLp.lean 4 declarations
- KahlerCofactorDivergence.lean 17 declarations
- KahlerEnergyChain.lean 5 declarations
- KahlerEnergyCutoff.lean 3 declarations
- KahlerEnergyProduct.lean 5 declarations
- KahlerGradientCoercivity.lean 6 declarations
- KahlerGradientEnergy.lean 9 declarations
- KahlerGreenIdentity.lean 6 declarations
- KahlerIntegralPos.lean 2 declarations
- KahlerIntegration.lean 11 declarations
- KahlerL2Comparison.lean 4 declarations
- KahlerLocalL2Comparison.lean 5 declarations
- KahlerPoincare.lean 1 declarations
- KahlerPoissonL2.lean 3 declarations
- KahlerSobolev.lean 3 declarations
- KahlerSobolevLocal.lean 5 declarations
- KahlerVolumeMeasure.lean 5 declarations
- KahlerVolumeVariation.lean 9 declarations
- LocalDeterminantBound.lean 4 declarations
- LocalDeterminantEquation.lean 7 declarations
- LocalDeterminantGain.lean 3 declarations
- LocalKahlerEnergy.lean 19 declarations
- LocalizedPathData.lean 8 declarations
- LpPowerBounds.lean 4 declarations
- MatrixCofactorOrder.lean 7 declarations
- MatrixCompactBounds.lean 5 declarations
- MatrixComponentBounds.lean 5 declarations
- MatrixDifferentialNew.lean 15 declarations
- MatrixWirtinger.lean 15 declarations
- MatrixWirtingerExtra.lean 6 declarations
- MatrixWirtingerSecond.lean 7 declarations
- MomentBoundPointwise.lean 1 declarations
- MongeAmpereC0.lean 2 declarations
- MongeAmpereEnergy.lean 11 declarations
- MongeAmpereL2.lean 3 declarations
- MongeAmpereMoments.lean 8 declarations
- MongeAmperePowerEnergy.lean 17 declarations
- MoserIteration.lean 1 declarations
- NormalizeVolumePath.lean 3 declarations
- PathLocalGain.lean 9 declarations
- PathLocalizedDensity.lean 6 declarations
- PathLocalizedMetricBounds.lean 3 declarations
- PathUniformAtlas.lean 8 declarations
- PathUniformForcing.lean 4 declarations
- PathUniformHigher.lean 4 declarations
- PathUniformSobolevBase.lean 4 declarations
- PositiveOpenness.lean 3 declarations
- PositivePathClosedness.lean 3 declarations
- PositivePathLimit.lean 5 declarations
- PositivePathOpenness.lean 4 declarations
- PowerDual.lean 5 declarations
- PowerIntegration.lean 4 declarations
- PrescribedPotential.lean 1 declarations
- PrescribedRicci.lean 13 declarations
- RoughCutoff.lean 6 declarations
- RoughEllipticGain.lean 3 declarations
- SchwartzHessianWords.lean 10 declarations
- SmoothLocalInverse.lean 4 declarations
- SmoothPathLimit.lean 4 declarations
- SmoothPositivePath.lean 4 declarations
- SobolevCommutatorBound.lean 6 declarations
- SobolevFamilyBounds.lean 3 declarations
- SobolevInterpolation.lean 6 declarations
- TameApproximation.lean 8 declarations
- TameCofactorGain.lean 4 declarations
- TameLimit.lean 3 declarations
- TameLocalInverse.lean 9 declarations
- TameRoughInverse.lean 2 declarations
- TameStability.lean 6 declarations
- TensorEnergyBounds.lean 3 declarations
- TraceCauchySchwarz.lean 2 declarations
- TraceEntryBounds.lean 4 declarations
- TraceMaximum.lean 5 declarations
- UniformCalabi.lean 2 declarations
- UniformChernLu.lean 3 declarations
- UniformCoefficientExtension.lean 3 declarations
- UniformCoefficientOscillation.lean 4 declarations
- UniformDeterminantRemainder.lean 3 declarations
- UniformFrozenEstimate.lean 6 declarations
- UniformL2.lean 8 declarations
- UniformLocalGain.lean 5 declarations
- UniformLocalH2.lean 1 declarations
- UniformMetricBounds.lean 1 declarations
- UniformPathPatches.lean 1 declarations
- UniformSchwartz.lean 11 declarations
- VolumePathRicci.lean 4 declarations
- WeightedMongeAmpereEnergy.lean 3 declarations
- WirtingerScalar.lean 11 declarations