WIP: Import Riemannian curvature and geometric analysis toward Ricci flow

LeanPool/PoincareGeometry/AlmostSchur.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Arthur Freitas Ramos and coauthors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
+-/
+
+/-
+Original copyright notice:
+Copyright (c) 2026 Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz. All rights
+reserved.
+-/
+
+module
+public import LeanPool.PoincareGeometry.AlmostSchur.GeometryComparison
+public import LeanPool.PoincareGeometry.AlmostSchur.Gradient
+public import LeanPool.PoincareGeometry.AlmostSchur.Hessian
+public import LeanPool.PoincareGeometry.AlmostSchur.HilbertSchmidt
+public import LeanPool.PoincareGeometry.AlmostSchur.HessianNorm
+public import LeanPool.PoincareGeometry.AlmostSchur.Volume
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalIntegration
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricDensity
+public import LeanPool.PoincareGeometry.AlmostSchur.DensityDerivative
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalMetricDivergence
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalEnergy
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartMetric
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartIntegration
+public import LeanPool.PoincareGeometry.AlmostSchur.GlobalMeasure
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.NormalizedMeasure
+public import LeanPool.PoincareGeometry.AlmostSchur.VolumeIntegration
+public import LeanPool.PoincareGeometry.AlmostSchur.OpenDomainIntegration
+public import LeanPool.PoincareGeometry.AlmostSchur.ConnectionCoordinates
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricConnectionCoordinates
+public import LeanPool.PoincareGeometry.AlmostSchur.TorsionCoordinates
+public import LeanPool.PoincareGeometry.AlmostSchur.DivergenceCoordinates
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartFlux
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartGreen
+public import LeanPool.PoincareGeometry.AlmostSchur.DivergenceRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.GlobalGreen
+public import LeanPool.PoincareGeometry.AlmostSchur.GradientRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.GlobalEnergy
+public import LeanPool.PoincareGeometry.AlmostSchur.HessianSymmetry
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyKernel
+public import LeanPool.PoincareGeometry.AlmostSchur.MeanZeroEnergy
+public import LeanPool.PoincareGeometry.AlmostSchur.DensityComparison
+public import LeanPool.PoincareGeometry.AlmostSchur.SobolevReconstruction
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakDerivativeMollification
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakKernelLocal
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartNormBounds
+public import LeanPool.PoincareGeometry.AlmostSchur.SobolevCompactness
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakKernelGluing
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalizationGradient
+public import LeanPool.PoincareGeometry.AlmostSchur.GradientL2
+public import LeanPool.PoincareGeometry.AlmostSchur.L2WeakLimit
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartL2Pullback
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartDerivativeBound
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalizationEnergy
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyAlgebra
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyCompactness
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartWeakKernel
+public import LeanPool.PoincareGeometry.AlmostSchur.PoincareCountersequence
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakChartLimit
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergySpace
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartLpRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.Poincare
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyL2
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyL2Completion
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakPoisson
+public import LeanPool.PoincareGeometry.AlmostSchur.L2TestUniqueness
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyChartDerivative
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyChartKernel
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyMean
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyGreen
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyPairingCoefficients
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyPairingReconstruction
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyL2Injectivity
+public import LeanPool.PoincareGeometry.AlmostSchur.HilbertWeakLimit
+public import LeanPool.PoincareGeometry.AlmostSchur.UniformQuadraticBound
+public import LeanPool.PoincareGeometry.AlmostSchur.CoordinateEllipticity
+public import LeanPool.PoincareGeometry.AlmostSchur.MatrixInverseRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.CoordinateCoefficientRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.CovariantAlongRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.ThirdHessianCommutator
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartTestLift
+public import LeanPool.PoincareGeometry.AlmostSchur.CoordinateGradient
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyLocalVariational
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricHigherRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.DifferenceQuotientWeakDerivative
+public import LeanPool.PoincareGeometry.AlmostSchur.DifferenceQuotientAlgebra
+public import LeanPool.PoincareGeometry.AlmostSchur.CoordinateForcing
+public import LeanPool.PoincareGeometry.AlmostSchur.CoordinateWeakPoisson
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartTestEnergy
+public import LeanPool.PoincareGeometry.AlmostSchur.L2Multiplier
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartCutoff
+public import LeanPool.PoincareGeometry.AlmostSchur.DifferenceQuotientProduct
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyCutoffGraph
+public import LeanPool.PoincareGeometry.AlmostSchur.TestGraphDifferenceQuotient
+public import LeanPool.PoincareGeometry.AlmostSchur.TestGraphCutoff
+public import LeanPool.PoincareGeometry.AlmostSchur.TestGraphVariational
+public import LeanPool.PoincareGeometry.AlmostSchur.ThirdHessianSymmetry
+public import LeanPool.PoincareGeometry.AlmostSchur.BochnerFluxRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.CovariantTraceDerivative
+public import LeanPool.PoincareGeometry.AlmostSchur.RawBochnerFlux
+public import LeanPool.PoincareGeometry.AlmostSchur.TestGraphUniformQuotient
+public import LeanPool.PoincareGeometry.AlmostSchur.IntegratedRawBochner
+public import LeanPool.PoincareGeometry.AlmostSchur.MatrixBilinearBound
+public import LeanPool.PoincareGeometry.AlmostSchur.EnergyAbsorption
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalWeakPoissonGraph
+public import LeanPool.PoincareGeometry.AlmostSchur.TestedDifferenceQuotient
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalTestedQuotient
+public import LeanPool.PoincareGeometry.AlmostSchur.L2BilinearIntegral
+public import LeanPool.PoincareGeometry.AlmostSchur.L2FiniteFamily
+public import LeanPool.PoincareGeometry.AlmostSchur.L2MatrixForm
+public import LeanPool.PoincareGeometry.AlmostSchur.CutoffPlateau
+public import LeanPool.PoincareGeometry.AlmostSchur.CutoffEnergyEstimate
+public import LeanPool.PoincareGeometry.AlmostSchur.WeightedFluxTest
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalQuotientEnergyEstimate
+public import LeanPool.PoincareGeometry.AlmostSchur.CutoffQuotientFields
+public import LeanPool.PoincareGeometry.AlmostSchur.InteriorCoefficientMasks
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakDerivativeBootstrap
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalH2QuotientBound
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakPoissonH2Bound
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalizedDerivativeExtraction
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakPoissonSecondDerivatives
+public import LeanPool.PoincareGeometry.AlmostSchur.PostH2Bootstrap
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakPoissonH2Jet
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakJetRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricTorsionCorrection
+public import LeanPool.PoincareGeometry.AlmostSchur.PointwiseConnection
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaCorrection
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaConnection
+public import LeanPool.PoincareGeometry.AlmostSchur.KoszulFormula
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricDualFrame
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaBochner
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaIntegratedBochner
+public import LeanPool.PoincareGeometry.AlmostSchur.CurvatureVendor.ContractedBianchiBridge
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalCurvatureExtensions
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalCurvatureTensor
+public import LeanPool.PoincareGeometry.AlmostSchur.BundledRicciBochner
+public import LeanPool.PoincareGeometry.AlmostSchur.HilbertSchmidtPairing
+public import LeanPool.PoincareGeometry.AlmostSchur.AlmostSchurAlgebra
+public import LeanPool.PoincareGeometry.AlmostSchur.IntegratedTraceFreeHessian
+public import LeanPool.PoincareGeometry.AlmostSchur.NonnegativeRicciBochner
+public import LeanPool.PoincareGeometry.AlmostSchur.ChartTestLiftRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.ManifoldTestUniqueness
+public import LeanPool.PoincareGeometry.AlmostSchur.MetricDualFrameTwo
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaRegularityTwo
+public import LeanPool.PoincareGeometry.AlmostSchur.EndomorphismFrameRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.CurvatureRicciRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.RicciTraceDerivative
+public import LeanPool.PoincareGeometry.AlmostSchur.ScalarCurvatureTraceDerivative
+public import LeanPool.PoincareGeometry.AlmostSchur.LeviCivitaBianchiCore
+public import LeanPool.PoincareGeometry.AlmostSchur.CurvatureDerivativeComparison
+public import LeanPool.PoincareGeometry.AlmostSchur.ContractedBianchiActual
+public import LeanPool.PoincareGeometry.AlmostSchur.WeightedFourierRegularity
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakJetFourierEstimate
+public import LeanPool.PoincareGeometry.AlmostSchur.WeakJetFourierRepresentative
+public import LeanPool.PoincareGeometry.AlmostSchur.LocalizedWeakJetGraph
+public import LeanPool.PoincareGeometry.AlmostSchur.ArbitraryWeakPoissonJets
+public import LeanPool.PoincareGeometry.AlmostSchur.SmoothWeakPoisson
+public import LeanPool.PoincareGeometry.AlmostSchur.AlmostSchurBound
+public import LeanPool.PoincareGeometry.AlmostSchur.AlmostSchurFinal
+public import LeanPool.PoincareGeometry.AlmostSchur.AlmostSchurEquality
+public import LeanPool.PoincareGeometry.RellichKondrachov.Geometry.Manifold.Sobolev.RellichKondrachov
+public import LeanPool.PoincareGeometry.RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Rellich
+public import LeanPool.PoincareGeometry.RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.SupportedH1
+public import LeanPool.PoincareGeometry.RellichKondrachov.MeasureTheory.Function.LpSpace.ExtendByZeroRangeEquiv
+
+/-! # Almost Schur -/