OAI/Geometry/Kahler/
1380 declarations, 0 contain sorry, 0 declared as axioms; 119 files
Files
- BaseAdaptedHopf.lean 9 declarations
- BaseAnisotropic.lean 5 declarations
- BaseCauchyJets.lean 4 declarations
- BaseCentralComparison.lean 5 declarations
- BaseCentralSecond.lean 3 declarations
- BaseChartJets.lean 2 declarations
- BaseChartLow.lean 4 declarations
- BaseChartNormalization.lean 7 declarations
- BaseChartScale.lean 3 declarations
- BaseChartSeries.lean 3 declarations
- BaseChartUniform.lean 3 declarations
- BaseCircleLog.lean 4 declarations
- BaseCirclePowerLog.lean 8 declarations
- BaseCompositionJets.lean 4 declarations
- BaseCorrectionDifferential.lean 3 declarations
- BaseCorrectionEstimate.lean 4 declarations
- BaseCorrectionMoments.lean 7 declarations
- BaseDensityBandwidth.lean 6 declarations
- BaseDensityDefinitions.lean 13 declarations
- BaseDensityFourier.lean 7 declarations
- BaseDensityInduction.lean 2 declarations
- BaseDensityLowMoments.lean 5 declarations
- BaseDensityMeasure.lean 5 declarations
- BaseDensityMoments.lean 4 declarations
- BaseDensityPatchEstimates.lean 5 declarations
- BaseDensityScales.lean 5 declarations
- BaseDensityStep.lean 3 declarations
- BaseDensityStepSupport.lean 3 declarations
- BaseDensityTheorem.lean 1 declarations
- BaseDensityThreshold.lean 2 declarations
- BaseDensityUpdate.lean 4 declarations
- BaseGaussian.lean 8 declarations
- BaseHessianJet.lean 8 declarations
- BaseHopf.lean 25 declarations
- BaseHorizontalArc.lean 6 declarations
- BaseHorizontalGeometry.lean 5 declarations
- BaseJetNorms.lean 11 declarations
- BaseLaterComparison.lean 3 declarations
- BaseLaterMoments.lean 3 declarations
- BaseLaterNegative.lean 2 declarations
- BaseLocalSmoothSeries.lean 3 declarations
- BaseLocalSmoothSeriesOn.lean 3 declarations
- BaseLogApproximation.lean 14 declarations
- BaseLogBounds.lean 1 declarations
- BaseLogFactor.lean 11 declarations
- BaseLogJetBounds.lean 1 declarations
- BaseLogPhase.lean 5 declarations
- BaseLogTests.lean 21 declarations
- BaseMeans.lean 14 declarations
- BaseMinorant.lean 3 declarations
- BaseModelParameters.lean 4 declarations
- BaseModelSign.lean 11 declarations
- BaseNegativeScaleBound.lean 2 declarations
- BaseNegativeThreshold.lean 3 declarations
- BaseOffPatchMean.lean 4 declarations
- BaseOrbitGrowth.lean 2 declarations
- BasePacking.lean 10 declarations
- BasePatchComparison.lean 3 declarations
- BasePatchDecomposition.lean 5 declarations
- BasePatchModel.lean 8 declarations
- BasePatchPhase.lean 5 declarations
- BasePatches.lean 11 declarations
- BasePeakBounds.lean 4 declarations
- BasePhaseAveraging.lean 7 declarations
- BasePhaseDerivatives.lean 6 declarations
- BasePhaseDifferential.lean 5 declarations
- BasePhaseFourier.lean 17 declarations
- BasePhaseMoments.lean 3 declarations
- BasePhaseReal.lean 3 declarations
- BasePhaseSupport.lean 13 declarations
- BasePolynomialChange.lean 3 declarations
- BasePotentialControl.lean 3 declarations
- BasePotentialSmooth.lean 5 declarations
- BaseProfileBounds.lean 3 declarations
- BaseProfiles.lean 24 declarations
- BaseProjective.lean 19 declarations
- BaseRadialCancellation.lean 3 declarations
- BaseRadialLaw.lean 7 declarations
- BaseRadialMeasure.lean 21 declarations
- BaseRadialModelError.lean 4 declarations
- BaseRadialMoments.lean 18 declarations
- BaseRadialPatch.lean 9 declarations
- BaseRadialSubstitution.lean 4 declarations
- BaseRadii.lean 5 declarations
- BaseRootAveraging.lean 4 declarations
- BaseScaleSum.lean 4 declarations
- BaseSeriesBounds.lean 3 declarations
- BaseShiftAveraging.lean 3 declarations
- BaseSphere.lean 12 declarations
- BaseTestAveraging.lean 3 declarations
- BaseTestSystem.lean 2 declarations
- BaseWeightedDerivative.lean 14 declarations
- Definitions.lean 39 declarations
- HartogsCharts.lean 13 declarations
- HartogsCompletenessSupport.lean 13 declarations
- HartogsCurvature.lean 58 declarations
- HartogsCurvatureContinuity.lean 7 declarations
- HartogsErrorBounds.lean 8 declarations
- HartogsFrame.lean 12 declarations
- HartogsGauge.lean 36 declarations
- HartogsGaugeTransfer.lean 4 declarations
- HartogsJetLinearity.lean 8 declarations
- HartogsJets.lean 29 declarations
- HartogsLiftedJets.lean 20 declarations
- HartogsMatrixBounds.lean 5 declarations
- HartogsModelBridge.lean 31 declarations
- HartogsNormalBlocks.lean 18 declarations
- HartogsNormalCurvature.lean 7 declarations
- HartogsNormalJets.lean 18 declarations
- HartogsNormalTables.lean 13 declarations
- HartogsPinching.lean 1 declarations
- HartogsTensorSymmetry.lean 7 declarations
- HartogsTopologySupport.lean 10 declarations
- HartogsTransfer.lean 2 declarations
- HartogsTransferTools.lean 10 declarations
- Main.lean 2 declarations
- MetricCalculus.lean 134 declarations
- Obstruction.lean 19 declarations
- PinchingCompact.lean 267 declarations