`OAI/Analysis/CircleDomains/Sobolev/`

1442 declarations, 0 contain sorry, 0 declared as axioms; 535 files

Files

ACLWeakDerivatives.lean 2 declarations
ActualLocalIntegrability.lean 5 declarations
AdmissibleL2Convex.lean 2 declarations
AdmissibleWeakLimit.lean 1 declarations
AffineLIntegral.lean 2 declarations
AffineLpTransport.lean 2 declarations
AffineSobolevWitness.lean 1 declarations
AnnulusStokes.lean 1 declarations
AppendingEnergyTolerance.lean 2 declarations
ApproximateCurveDerivative.lean 1 declarations
ArgumentCircleIntegral.lean 7 declarations
AverageSquareBound.lean 1 declarations
AverageSubsets.lean 2 declarations
AxisSwapEnergy.lean 11 declarations
BandCoarea.lean 4 declarations
BarrierDifferentialError.lean 2 declarations
BarrierEnergyAssembly.lean 2 declarations
BarrierL2Error.lean 1 declarations
BorelSobolevGradient.lean 3 declarations
BoundedContinuousL2Dual.lean 1 declarations
BoundedDensityEnergy.lean 2 declarations
BoundedEnergyWeakClosure.lean 3 declarations
BoundedIntervalIntegral.lean 1 declarations
BoundedLocalBranches.lean 6 declarations
BoundedMaximalL2.lean 1 declarations
BoundedRepresentative.lean 2 declarations
BoundedSobolevChain.lean 2 declarations
BoundedUpperIntegral.lean 4 declarations
BoundedWeakIdentification.lean 1 declarations
BoundedWeakRange.lean 1 declarations
CircleAverageAngularIntegral.lean 1 declarations
CircleBranchEnergy.lean 6 declarations
CircleComplexEnergy.lean 2 declarations
CircleDifferential.lean 17 declarations
CircleDifferentialClosed.lean 2 declarations
CircleEnergy.lean 5 declarations
CircleEnergyChange.lean 1 declarations
CircleFilledEnergy.lean 7 declarations
CircleGradientSize.lean 2 declarations
CircleIntegralCongruence.lean 1 declarations
CirclePartitionEnergy.lean 2 declarations
CirclePartitionGradient.lean 3 declarations
CirclePartitionSmoothing.lean 4 declarations
CircleProjectionIntegrable.lean 5 declarations
CircleSmoothingBands.lean 4 declarations
CircleSmoothingTolerance.lean 1 declarations
CircleStaircaseGradient.lean 3 declarations
CircleWeightedCoarea.lean 1 declarations
ClippedDirectionalDerivative.lean 3 declarations
ClippedScalarEnergy.lean 5 declarations
ClosedDiskIntegral.lean 1 declarations
ClosedGapIntegrals.lean 3 declarations
CoareaInput.lean 18 declarations
CoareaL2Errors.lean 1 declarations
CoareaL2Weight.lean 1 declarations
CoareaLevels.lean 6 declarations
CoareaSummableErrors.lean 1 declarations
CoareaZeroProduct.lean 2 declarations
ColoredGridEnergy.lean 2 declarations
CompactCutoffEnergy.lean 1 declarations
CompactIntegralComparison.lean 1 declarations
CompactMeasureL2Plan.lean 1 declarations
CompactMollifierSampling.lean 4 declarations
CompactPhysicalFiberCoarea.lean 4 declarations
CompactSobolevCutoff.lean 3 declarations
CompactSobolevHeightModulus.lean 1 declarations
CompactSobolevJacobian.lean 3 declarations
CompactWeakDerivativeIntegral.lean 3 declarations
CompactWeakExtension.lean 1 declarations
ComplementWeakGradient.lean 1 declarations
ComplexCoareaControls.lean 5 declarations
ComplexCoareaJacobian.lean 2 declarations
ComplexCovectorEnergy.lean 4 declarations
ComplexCovectorWedge.lean 3 declarations
ComplexGradientError.lean 2 declarations
ComplexLocalScalarWitness.lean 1 declarations
ComplexLocalSobolevTransport.lean 4 declarations
ComplexPhysicalGradient.lean 2 declarations
ComplexPolarDifferential.lean 3 declarations
ComplexRealEnergy.lean 2 declarations
ComplexScalarEnergy.lean 3 declarations
ComplexSobolevTransport.lean 4 declarations
ComplexTangentFrame.lean 4 declarations
ComplexWeakDirectionalTransport.lean 1 declarations
ComplexWeakGradient.lean 5 declarations
ComplexWedgeIntegral.lean 1 declarations
ConfigurationHitIntegral.lean 2 declarations
ConformalSobolevEnergyIdentity.lean 1 declarations
ContinuousScalarSobolev.lean 3 declarations
CoordinateEnergy.lean 7 declarations
CoordinateEstimates.lean 13 declarations
CoordinateGradientSize.lean 3 declarations
CoordinateSquares.lean 6 declarations
CountableEnergyNeighborhoods.lean 1 declarations
CountableValueFlattening.lean 1 declarations
CovectorMetric.lean 7 declarations
CurveAreaStability.lean 1 declarations
CurveCoareaInput.lean 4 declarations
CutoffEnergyAlgebra.lean 2 declarations
DensityL2.lean 2 declarations
DerivativeLipschitzPartition.lean 2 declarations
DifferentiableCriticalFibers.lean 2 declarations
DifferentiableCriticalPieces.lean 1 declarations
DifferentiableCurveLength.lean 3 declarations
DustSmoothingTolerance.lean 5 declarations
DustSobolevExtension.lean 1 declarations
EnergyBallCover.lean 1 declarations
EnergyChangeCoordinates.lean 4 declarations
EnergyLocalization.lean 1 declarations
EnergyTransportIntegrability.lean 4 declarations
ExactSobolevLinePayment.lean 1 declarations
ExtendedDensityL2.lean 2 declarations
ExtendedWeightedCoarea.lean 2 declarations
ExteriorAngularEnergy.lean 1 declarations
ExteriorAnnulusArea.lean 2 declarations
ExteriorAnnulusEnergy.lean 2 declarations
ExteriorAreaBoundProof.lean 2 declarations
ExteriorCircleAreaContinuity.lean 2 declarations
ExteriorCircleAreaPositive.lean 3 declarations
ExteriorCircleEnergy.lean 2 declarations
ExteriorCoefficientAreaProof.lean 2 declarations
ExteriorDerivativeMean.lean 6 declarations
ExteriorOmittedAreaInput.lean 1 declarations
FilledScalarEnergy.lean 3 declarations
FilledScalarGlobalEnergy.lean 5 declarations
FilledScalarL2.lean 2 declarations
FilledScalarSliceDerivative.lean 2 declarations
FilledScalarTestIntegrals.lean 1 declarations
FilledSmoothBarrier.lean 1 declarations
FiniteEnergy.lean 2 declarations
FiniteGreenAssembly.lean 3 declarations
FiniteHitSquareEnergy.lean 3 declarations
FiniteHoleIntegral.lean 1 declarations
FiniteOffsetStokes.lean 4 declarations
FinitePeriodStokes.lean 3 declarations
FiniteSmoothCover.lean 1 declarations
FiniteSphericalArea.lean 2 declarations
FiniteTransferEnergy.lean 1 declarations
FixedWidthIntegrability.lean 4 declarations
GramMetric.lean 6 declarations
HalfPlaneDerivativeBound.lean 6 declarations
HeightEnergyModulus.lean 2 declarations
HeightSmoothApproximation.lean 1 declarations
HeightZeroEnergyLimit.lean 1 declarations
HilbertWeakConvexApproximation.lean 2 declarations
HilbertWeakSubsequence.lean 1 declarations
HolomorphicInjOnDerivative.lean 6 declarations
HolomorphicScalarEnergy.lean 3 declarations
HolomorphicWeakRows.lean 3 declarations
IncrementDerivativeBound.lean 2 declarations
IndicatorL2Energy.lean 1 declarations
IntegralLineAbsoluteContinuity.lean 2 declarations
IntegralPaymentAbsoluteContinuity.lean 2 declarations
InteriorLocalGreen.lean 1 declarations
InverseChartCoarea.lean 5 declarations
InverseOnDerivativeField.lean 1 declarations
InverseOnDifferentiation.lean 3 declarations
InversePieceCoarea.lean 2 declarations
InversePieceJacobian.lean 4 declarations
InversePowerAnnulusIntegral.lean 1 declarations
JordanSignedArea.lean 2 declarations
L2AdditiveMajorant.lean 1 declarations
L2DominatedAeSubsequence.lean 1 declarations
L2DominatingSubsequence.lean 1 declarations
L2PositiveTests.lean 2 declarations
L2ProductConvergence.lean 2 declarations
L2Series.lean 1 declarations
L2SummableMajorant.lean 1 declarations
L2ThreeTermBound.lean 3 declarations
L2WeakSubsequence.lean 1 declarations
L2WeightedErrorSeries.lean 2 declarations
LengthContentLipschitz.lean 1 declarations
LiftDifferentials.lean 8 declarations
LineDerivativeLocality.lean 2 declarations
LineLIntegralAbsoluteContinuity.lean 1 declarations
LineLIntegralDerivativeBound.lean 1 declarations
LipschitzArclengthBounds.lean 4 declarations
LipschitzCoareaProof.lean 1 declarations
LipschitzCurveLength.lean 1 declarations
LipschitzFiberIntegralBound.lean 1 declarations
LipschitzIntervalPaths.lean 11 declarations
LipschitzLengthFiberMajorant.lean 2 declarations
LipschitzMappedArclength.lean 3 declarations
LipschitzMappedCost.lean 2 declarations
LipschitzNullFibers.lean 2 declarations
LipschitzPieceGradient.lean 2 declarations
LipschitzScalarCoarea.lean 2 declarations
LocalArgumentBranch.lean 3 declarations
LocalBoundedSobolevChain.lean 2 declarations
LocalComplexJacobianForm.lean 4 declarations
LocalComplexWeyl.lean 3 declarations
LocalComplexWitness.lean 4 declarations
LocalCoordinateMetric.lean 3 declarations
LocalDensityIntegrability.lean 4 declarations
LocalDerivativeCover.lean 2 declarations
LocalEnergyOneEndedSplicing.lean 1 declarations
LocalEnergyTwoEndedSplicing.lean 1 declarations
LocalGradientIntegrability.lean 2 declarations
LocalGradientMajorant.lean 1 declarations
LocalImageAreaForm.lean 1 declarations
LocalLiftSmoothing.lean 1 declarations
LocalMollificationCongruence.lean 3 declarations
LocalPairChainRule.lean 1 declarations
LocalPairChainWitness.lean 1 declarations
LocalScalarEnergy.lean 2 declarations
LocalSmoothExtension.lean 1 declarations
LocalSmoothPartition.lean 2 declarations
LocalSobolevClassicalPartials.lean 1 declarations
LocalSobolevGluing.lean 1 declarations
LocalSobolevGraphNull.lean 1 declarations
LocalSobolevHeightModulus.lean 1 declarations
LocalSobolevJacobianReplacement.lean 3 declarations
LocalSobolevLipschitzCover.lean 2 declarations
LocalSobolevNullLevels.lean 2 declarations
LocalSobolevPoincare.lean 1 declarations
LocalSobolevSmoothing.lean 4 declarations
LocalWeakBarrierBound.lean 1 declarations
LocalWeakGradientEnergy.lean 3 declarations
LocalZeroGradientConstant.lean 2 declarations
LocalizedJordanIntegral.lean 5 declarations
LocalizedPartitionEnergy.lean 1 declarations
LocalizedPotentialSmoothing.lean 1 declarations
LocalizedRealGradientNorm.lean 2 declarations
LocalizedSobolevRange.lean 1 declarations
LocallyFiniteL2Sum.lean 3 declarations
LocallySobolevACL.lean 2 declarations
LocallySobolevCoordinateFTC.lean 1 declarations
LocallySobolevPartials.lean 2 declarations
LogarithmicEnergyBound.lean 2 declarations
MarkedConfigurationIntegral.lean 1 declarations
MaximalTruncations.lean 11 declarations
MeanSmoothPhysicalCount.lean 1 declarations
MeasurableCircleGradient.lean 4 declarations
MeasurableLineDerivatives.lean 2 declarations
MeasurePlanWeakDuality.lean 1 declarations
MetricChartEnergy.lean 4 declarations
MetricComposition.lean 5 declarations
MetricEnergy.lean 6 declarations
MetricIntegral.lean 4 declarations
MetricInterpolation.lean 11 declarations
MetricTensor.lean 6 declarations
MixedCircuitSmoothness.lean 2 declarations
ModelBarrierGradient.lean 2 declarations
ModelLocalEnergy.lean 3 declarations
ModelPairBarrierEnergy.lean 1 declarations
ModelPriorityWeakError.lean 1 declarations
ModelRealEnergy.lean 2 declarations
ModelScalarEnergy.lean 3 declarations
ModelSmoothBarrier.lean 1 declarations
ModelUniformJointEnergy.lean 2 declarations
ModelUniformRowEnergy.lean 2 declarations
ModelWorkingGradients.lean 2 declarations
MollificationEnergy.lean 3 declarations
MollificationMovingPoint.lean 1 declarations
MonotoneL2Limit.lean 1 declarations
NonnegativeMaximalL2.lean 1 declarations
NormalizedArgumentDifferential.lean 3 declarations
NormalizedCircleEnergy.lean 1 declarations
OpenMeanCircleSmoothing.lean 1 declarations
OriginalDomainMetric.lean 4 declarations
PairKernelEnergy.lean 1 declarations
PairedEnergyCauchy.lean 2 declarations
ParallelJumpIntegral.lean 1 declarations
PartitionApproximation.lean 1 declarations
PartitionErrorSum.lean 3 declarations
PartitionGradientBound.lean 4 declarations
PartitionGradientEnergy.lean 1 declarations
PartitionGradientIdentity.lean 2 declarations
PartitionLiftApproximation.lean 2 declarations
PartitionLiftErrorSum.lean 3 declarations
PartitionLocalDerivatives.lean 1 declarations
PartitionMixing.lean 8 declarations
PartitionPlateaus.lean 2 declarations
PartitionTestDecomposition.lean 1 declarations
PartitionWeakGradient.lean 2 declarations
PatchBandPreservation.lean 6 declarations
PeriodBranchPhysicalEnergy.lean 1 declarations
PeriodWeightedCoarea.lean 1 declarations
PeriodizedLevels.lean 11 declarations
PhysicalCauchyRiemann.lean 3 declarations
PhysicalCircleSmoothing.lean 1 declarations
PhysicalCoareaCoordinates.lean 4 declarations
PhysicalCoareaTransport.lean 2 declarations
PhysicalCoordinateCoarea.lean 2 declarations
PhysicalCoordinateLines.lean 7 declarations
PhysicalFieldCoarea.lean 4 declarations
PhysicalLineDifferentiation.lean 2 declarations
PhysicalLipschitzCoarea.lean 2 declarations
PhysicalMeanIndexSobolev.lean 2 declarations
PhysicalPartitionBands.lean 1 declarations
PhysicalRoundIntegrals.lean 7 declarations
PhysicalSamplingPartition.lean 2 declarations
PhysicalSobolevLipschitzCover.lean 2 declarations
PlanarDifferentialEnergy.lean 2 declarations
PlanarEnergyChange.lean 3 declarations
PlanarGradientDensity.lean 12 declarations
PlanarSliceIntegrals.lean 7 declarations
PlanarSobolevTransport.lean 2 declarations
PlaneCovectorEnergy.lean 2 declarations
PolarAnnulusEnergy.lean 1 declarations
PolarAnnulusIntegral.lean 2 declarations
PolarDiskIntegral.lean 1 declarations
PositiveLocalAverages.lean 6 declarations
PositiveMollification.lean 2 declarations
PositivePartitionSmoothing.lean 1 declarations
PositiveSobolevApproximation.lean 13 declarations
PotentialCutoffSmoothing.lean 1 declarations
PotentialGlobalSmoothing.lean 1 declarations
PotentialLineDerivativeBound.lean 2 declarations
PotentialLineRegularity.lean 1 declarations
PotentialPartitionSmoothing.lean 1 declarations
PotentialPhysicalSmoothing.lean 1 declarations
PotentialRectangleACL.lean 4 declarations
PotentialRectangleDerivativeBounds.lean 1 declarations
PotentialRectangleSobolev.lean 1 declarations
PotentialSobolevWitness.lean 1 declarations
PotentialWeightedSobolev.lean 1 declarations
PrincipalCircleArea.lean 4 declarations
PrincipalCircleAreaEstimate.lean 4 declarations
PrincipalCircleAreaLimit.lean 1 declarations
PrincipalLocalizedDerivativeError.lean 1 declarations
PrincipalScalarEnergy.lean 1 declarations
PrincipalScalarWeakLimit.lean 6 declarations
PrincipalSmoothApproximation.lean 4 declarations
PrincipalSmoothExterior.lean 4 declarations
PrincipalSmoothLimit.lean 3 declarations
PrincipalWeakDirections.lean 5 declarations
PriorFilledSmoothBarrier.lean 1 declarations
PriorSmoothedCompatibility.lean 1 declarations
PriorityDerivativeError.lean 1 declarations
PriorityL2Approximation.lean 1 declarations
PriorityL2Error.lean 2 declarations
PriorityLocalDerivative.lean 2 declarations
PrioritySmooth.lean 3 declarations
PrioritySupportEnergy.lean 1 declarations
ProductAverage.lean 5 declarations
QuarterTurnEnergy.lean 6 declarations
QuasiconformalSobolev.lean 7 declarations
RationalAbsoluteContinuity.lean 2 declarations
RationalLineDerivative.lean 1 declarations
RealCoordinateDifferential.lean 2 declarations
RealCoordinateLines.lean 11 declarations
RealGradientNorm.lean 2 declarations
RealGradientTransport.lean 3 declarations
RealPolarAnnulus.lean 3 declarations
RectangleDerivativeRepresentatives.lean 5 declarations
RectanglePoincare.lean 2 declarations
RectangleSobolev.lean 2 declarations
RectangularL2.lean 5 declarations
RectangularPoincare.lean 1 declarations
RefinedPhysicalSampling.lean 1 declarations
RefinedShrinkingRectanglePartition.lean 1 declarations
RegularAnnulusStokes.lean 1 declarations
RegularCoareaNeighborhood.lean 2 declarations
RegularCoareaProof.lean 1 declarations
RegularOffsetStokes.lean 1 declarations
RegularPieceCoarea.lean 3 declarations
RescaledBandEnergy.lean 2 declarations
RescaledScalarBump.lean 7 declarations
RestrictedWeakPairing.lean 1 declarations
RetainedSobolevContinuations.lean 2 declarations
RotatedRealEnergy.lean 4 declarations
RoundAnnulusGreen.lean 1 declarations
SardProof.lean 1 declarations
SavedBarrierEnergy.lean 1 declarations
SavedBarrierEnergySlack.lean 1 declarations
ScalarContinuationEnergy.lean 4 declarations
ScalarCutoffEnergy.lean 2 declarations
ScalarEnergyMeasure.lean 4 declarations
ScalarEnergySaturation.lean 1 declarations
ScalarFlattening.lean 6 declarations
ScalarFlatteningApproximation.lean 1 declarations
ScalarFlatteningEnergy.lean 8 declarations
ScalarFlatteningWeak.lean 1 declarations
ScalarImageEnergy.lean 1 declarations
ScalarImageGradient.lean 1 declarations
ScalarLocalLp.lean 5 declarations
ScalarModelExactEnergy.lean 1 declarations
ScalarRegularCoarea.lean 1 declarations
ScalarRegularCoordinates.lean 10 declarations
ScalarSobolevLimit.lean 1 declarations
ScalarWeakEnergy.lean 1 declarations
ScalarWeakLimitZeroSet.lean 1 declarations
ScalarWeakLimits.lean 4 declarations
ScaledCutoffEnergy.lean 6 declarations
ShrinkingAverageSupport.lean 2 declarations
ShrinkingHitEnergy.lean 3 declarations
ShrinkingOccupationEnergy.lean 3 declarations
ShrinkingRectangleCover.lean 2 declarations
ShrinkingRectanglePartition.lean 1 declarations
SliceDensityLp.lean 3 declarations
SmallEnergyCore.lean 3 declarations
SmallEnergyCutoff.lean 8 declarations
SmallGradientNeighborhood.lean 1 declarations
SmallSelectedBarrierEnergy.lean 1 declarations
SmallShrinkingRectanglePartition.lean 2 declarations
SmoothCircleOscillation.lean 5 declarations
SmoothClosedSliceImage.lean 1 declarations
SmoothCollarLowerBound.lean 1 declarations
SmoothContours.lean 8 declarations
SmoothCurveCoarea.lean 3 declarations
SmoothCurveImage.lean 2 declarations
SmoothCurveMeasurability.lean 1 declarations
SmoothCutoffLinePayment.lean 1 declarations
SmoothDiskGreen.lean 3 declarations
SmoothEnergyLimit.lean 1 declarations
SmoothExteriorReplacement.lean 1 declarations
SmoothFiniteTransfer.lean 3 declarations
SmoothImageArea.lean 4 declarations
SmoothImageScalar.lean 1 declarations
SmoothJordanExhaustion.lean 9 declarations
SmoothJordanNeighborhoods.lean 3 declarations
SmoothLineOscillation.lean 2 declarations
SmoothLocalWeakDerivative.lean 3 declarations
SmoothLogarithmicModulus.lean 3 declarations
SmoothMeanBandWeight.lean 2 declarations
SmoothMeanCircuit.lean 2 declarations
SmoothMeanCodeLevels.lean 1 declarations
SmoothMeanCollarApplication.lean 1 declarations
SmoothMeanCoordinateConstruction.lean 1 declarations
SmoothMeanGraphGeometry.lean 2 declarations
SmoothMeanPeriodConsequences.lean 2 declarations
SmoothMeanPeriodData.lean 2 declarations
SmoothMeanPhysicalBranches.lean 2 declarations
SmoothMeanRealRepresentative.lean 3 declarations
SmoothOpenImageMeasure.lean 1 declarations
SmoothPathIntersections.lean 3 declarations
SmoothPathOccupation.lean 3 declarations
SmoothPhysicalPullback.lean 5 declarations
SmoothPhysicalPullbackBounds.lean 5 declarations
SmoothPlaneEnergyTransport.lean 2 declarations
SmoothPlaneLinePayment.lean 1 declarations
SmoothPlaneSobolev.lean 4 declarations
SmoothPullbackFiniteEnergy.lean 1 declarations
SmoothRadialShrink.lean 12 declarations
SmoothRadialShrinkInverse.lean 2 declarations
SmoothRealLift.lean 3 declarations
SmoothRealSphereMaps.lean 16 declarations
SmoothRectangleExtension.lean 2 declarations
SmoothScalarCutoffWitness.lean 2 declarations
SmoothScalarWeakLimit.lean 2 declarations
SmoothSphereCharts.lean 6 declarations
SmoothSphereEquivalence.lean 6 declarations
SmoothTransportDifferenceEnergy.lean 1 declarations
SmoothWeakGradient.lean 2 declarations
SmoothWeightedL2Pullback.lean 2 declarations
SmoothedBarrierCompatibility.lean 1 declarations
SmoothedBarrierPlateaus.lean 1 declarations
SobolevBarrierCollapse.lean 1 declarations
SobolevCapacityBallCover.lean 1 declarations
SobolevCapacityCover.lean 1 declarations
SobolevCapacityMass.lean 1 declarations
SobolevCapacityScale.lean 1 declarations
SobolevClassicalPartials.lean 3 declarations
SobolevClosedLipschitzCover.lean 2 declarations
SobolevCoareaFiniteLevels.lean 2 declarations
SobolevCoareaProof.lean 2 declarations
SobolevConformalTransport.lean 2 declarations
SobolevCoordinateFTC.lean 2 declarations
SobolevEnergyMeasure.lean 2 declarations
SobolevGraphEnergy.lean 4 declarations
SobolevGraphEnergyRegular.lean 4 declarations
SobolevGraphLocalCover.lean 1 declarations
SobolevGraphNull.lean 1 declarations
SobolevHeightLevelNull.lean 2 declarations
SobolevJacobianLocality.lean 2 declarations
SobolevLengthCapacity.lean 1 declarations
SobolevLevelOscillation.lean 1 declarations
SobolevLinePayment.lean 1 declarations
SobolevLipschitzRepresentatives.lean 1 declarations
SobolevNullFibers.lean 2 declarations
SobolevNullLevels.lean 2 declarations
SobolevRangeBound.lean 1 declarations
SobolevRepresentative.lean 3 declarations
SobolevScalarCoarea.lean 3 declarations
SobolevTypicalLinePayment.lean 2 declarations
SourceArea.lean 5 declarations
SphereChartDerivativeDecay.lean 6 declarations
SphereChartLipschitz.lean 4 declarations
SphereCircleEnergy.lean 2 declarations
SphereRealDifferential.lean 6 declarations
SphereScalarLineSmooth.lean 2 declarations
SphericalAreaLocalization.lean 7 declarations
SphericalBallArea.lean 3 declarations
SphericalGradientEnergyNorm.lean 2 declarations
SphericalWeightedCoarea.lean 1 declarations
SquareAverageBounded.lean 2 declarations
SquareAverageComparison.lean 3 declarations
SquareAverageL2.lean 1 declarations
SquareOscillationLipschitz.lean 2 declarations
SquarePoincareEnergy.lean 2 declarations
StaircaseGradient.lean 2 declarations
StereographicDerivativeBound.lean 4 declarations
StrongGradientEnergyLimit.lean 1 declarations
StrongWeakPartialLimit.lean 1 declarations
SummableEnergyCutoffs.lean 3 declarations
SummableSobolevApproximation.lean 1 declarations
SupportedMetric.lean 2 declarations
TargetArea.lean 5 declarations
TensorAverageBound.lean 1 declarations
TensorEnergy.lean 15 declarations
ThreeL2WeakLimits.lean 1 declarations
TrackedGlobalWeakLimit.lean 1 declarations
TrackedTailGradient.lean 1 declarations
TransportedRealEnergy.lean 3 declarations
UniformLocalMollification.lean 1 declarations
UniformSobolevApproximation.lean 1 declarations
UniformSphericalBallArea.lean 4 declarations
VanishingL2Pairings.lean 1 declarations
VerticalFilledDerivative.lean 2 declarations
VerticalWeakConstant.lean 3 declarations
WeakBarrierEstimate.lean 1 declarations
WeakBarrierMeasurability.lean 2 declarations
WeakCovectorGradient.lean 6 declarations
WeakGradientAffineRescale.lean 1 declarations
WeakHeightIdentification.lean 3 declarations
WeakHeightNull.lean 1 declarations
WeakPairDifferential.lean 7 declarations
WeakPairEnergy.lean 2 declarations
WeakPairL2.lean 5 declarations
WeakPartialLocality.lean 3 declarations
WeakPartialPairingLimit.lean 3 declarations
WeakProbabilityMeasurability.lean 1 declarations
WedgeEnergy.lean 2 declarations
WedgeIntegrability.lean 5 declarations
WeightedCoareaFiniteUnion.lean 1 declarations
WeightedCoareaUnion.lean 3 declarations
WeightedDifferentiableCurve.lean 2 declarations
WeightedLipschitzCurve.lean 2 declarations
WeightedPlanarCoareaProof.lean 1 declarations
WeightedSmoothContours.lean 2 declarations
WeightedSobolevErrors.lean 5 declarations
WeightedSobolevTransport.lean 1 declarations
ZeroOffsetStokes.lean 1 declarations
ZeroWeakGradient.lean 1 declarations