`OAI/Analysis/CircleDomains/Modulus/`

787 declarations, 0 contain sorry, 0 declared as axioms; 266 files

Files

ActualOneEndedBudget.lean 3 declarations
ActualTwoEndedBudget.lean 3 declarations
ActualWedgeCost.lean 3 declarations
AdmissiblePathCost.lean 4 declarations
AffinePhysicalArclength.lean 1 declarations
AffineRectifiableLength.lean 3 declarations
ArcBoundaryPayment.lean 2 declarations
ArcReductionNormBounds.lean 3 declarations
AssignedStokesBudget.lean 1 declarations
AverageOscillation.lean 4 declarations
BallMaximalPayment.lean 2 declarations
BalloonLinePayment.lean 3 declarations
BandBudgetNorm.lean 1 declarations
BandIncidence.lean 11 declarations
BarrierCollapse.lean 3 declarations
BarrierConstruction.lean 1 declarations
BarrierErrorBudgets.lean 2 declarations
BarrierJumpLosses.lean 7 declarations
BarrierModulus.lean 1 declarations
BarrierPlateauGeometry.lean 3 declarations
BarrierRebase.lean 3 declarations
BarrierTrialMetric.lean 3 declarations
BilipschitzPathCost.lean 2 declarations
ChainPotentialOscillation.lean 6 declarations
CircleBoundaryOscillation.lean 3 declarations
CircleWedgeCost.lean 5 declarations
CodeFreeIncidence.lean 1 declarations
CodeModulusExtraction.lean 2 declarations
CollarConcatenationCost.lean 1 declarations
CompactBarrierData.lean 3 declarations
CompactBarrierProjection.lean 3 declarations
CompactContinuousImageModulus.lean 2 declarations
CompactMajorantSeparation.lean 1 declarations
CompatibleLevelBarrier.lean 4 declarations
CompatibleRealBarrier.lean 4 declarations
ComponentBarriers.lean 6 declarations
ConcatenatedIncidenceBounds.lean 3 declarations
ConfigurationAtomicNorm.lean 9 declarations
ConfigurationNorm.lean 5 declarations
ConformalNormalization.lean 6 declarations
ConstrainedCostCodes.lean 9 declarations
CostPerturbation.lean 10 declarations
CostSummands.lean 9 declarations
CountableConcatenationLength.lean 4 declarations
CountableImageIncidence.lean 9 declarations
CountablePhysicalCost.lean 3 declarations
CountablePhysicalLength.lean 3 declarations
CountablePositiveWeights.lean 1 declarations
CriticalFiberLength.lean 2 declarations
DisjointArcLengths.lean 3 declarations
DisjointBallPayments.lean 2 declarations
DisjointHolePayment.lean 1 declarations
DiskLinePayment.lean 3 declarations
DistinguishedStokesBudget.lean 3 declarations
DominatedLinePayment.lean 2 declarations
DustPriorBudgets.lean 4 declarations
DyadicTimeLength.lean 11 declarations
EventualFragmentBudget.lean 1 declarations
FilledFirstArrivalBarrier.lean 1 declarations
FilledScalarNormBounds.lean 2 declarations
FiniteBandNorm.lean 1 declarations
FiniteCircleBarrierCollapse.lean 2 declarations
FiniteCircleLinePayment.lean 2 declarations
FiniteCostChartPaths.lean 3 declarations
FiniteDiskSlicePayment.lean 2 declarations
FiniteGapPayment.lean 3 declarations
FiniteLengthTopology.lean 2 declarations
FiniteLevelPayments.lean 1 declarations
FiniteWedgeCosts.lean 10 declarations
FiniteWeightedCutoffs.lean 2 declarations
FirstArrivalBarrierPotential.lean 1 declarations
FirstExitFragmentBudget.lean 2 declarations
FixedCapacityCutoffs.lean 8 declarations
FixedCoreBarrierPayment.lean 1 declarations
FixedNormalOrientation.lean 2 declarations
FlexibleCirclePayment.lean 2 declarations
GridIncidence.lean 7 declarations
HausdorffPayment.lean 3 declarations
HeightNormalization.lean 1 declarations
HitNormTopology.lean 4 declarations
HolomorphicStrictNorm.lean 2 declarations
HyperspaceIncidence.lean 9 declarations
InitialWeightedCollar.lean 1 declarations
InteriorPhysicalCost.lean 5 declarations
InterleavedCollarCost.lean 3 declarations
InterposedWeightedCollars.lean 1 declarations
IntervalChartCost.lean 3 declarations
JoinedDomainCost.lean 1 declarations
JoinedJunctionCost.lean 3 declarations
JoinedPhysicalCost.lean 3 declarations
LaurentNormalization.lean 5 declarations
LengthContent.lean 4 declarations
LevelBarrierLocalizedNorm.lean 3 declarations
LevelBarrierOpenExclusion.lean 1 declarations
LevelBarrierRebase.lean 2 declarations
LevelBarrierSlackExclusion.lean 1 declarations
LevelIncidence.lean 6 declarations
LinePayment.lean 7 declarations
LinearChartWeight.lean 1 declarations
LocalBandIncidence.lean 3 declarations
LocalBandIntervalPayment.lean 1 declarations
LocalBandPathPayment.lean 2 declarations
LocalBandPhysicalPayment.lean 1 declarations
LocalGraphCapacity.lean 1 declarations
LocalPlateauPayment.lean 1 declarations
LocalRetainedBarrier.lean 1 declarations
LocalWeightedCollars.lean 1 declarations
LocalizedCirclePayment.lean 2 declarations
LocalizedGeometricPayment.lean 1 declarations
LocalizedNormalGreen.lean 2 declarations
LocalizedNormalGreenLower.lean 1 declarations
LocalizedTerminalPayment.lean 1 declarations
LoopOscillationMinimum.lean 9 declarations
MarkedConfigurationNorm.lean 7 declarations
MeanCoordinateBudget.lean 1 declarations
MeanIndexArcPayment.lean 1 declarations
MeanIndexOscillation.lean 1 declarations
MeanPeriodBudget.lean 2 declarations
MixedChainNormalization.lean 1 declarations
MobiusNormalization.lean 7 declarations
ModelPairBarrier.lean 4 declarations
ModelSelectedBarrier.lean 1 declarations
ModulusFiniteBallCut.lean 1 declarations
ModulusFiniteMesh.lean 1 declarations
ModulusNormBound.lean 1 declarations
NestedWeightedCollars.lean 1 declarations
NonsingularStokesBudget.lean 1 declarations
NormalBoxImage.lean 4 declarations
NormalChartJordanSides.lean 1 declarations
NormalFamilyInputs.lean 4 declarations
NormalStripImageGreen.lean 1 declarations
NormalStripRectangleGreen.lean 4 declarations
NormalizedArgument.lean 7 declarations
NormalizedArgumentBasic.lean 5 declarations
NormalizedAssignedEnds.lean 1 declarations
NormalizedComponentQuotient.lean 1 declarations
NormalizedComponentShrinking.lean 1 declarations
NormalizedLimitEquivalence.lean 4 declarations
NormalizedLimits.lean 6 declarations
NormalizedMarkedModels.lean 3 declarations
NormalizedMetricUniformization.lean 3 declarations
NormalizedSourceRepresentative.lean 2 declarations
NormalizedUniformBounds.lean 1 declarations
NormalizedUniformization.lean 2 declarations
NormedAffineLinePayment.lean 3 declarations
OneEndedFragmentBudget.lean 1 declarations
OpenGapPayment.lean 1 declarations
OrderedHolePayment.lean 1 declarations
OuterBarrierMargin.lean 1 declarations
PartialSimpleArcLength.lean 6 declarations
PathCostReference.lean 9 declarations
PathHausdorffLength.lean 2 declarations
PathIntervalOscillation.lean 7 declarations
PathLengthKernel.lean 4 declarations
PathLengthLocality.lean 9 declarations
PathVariation.lean 4 declarations
PeriodBandBudget.lean 2 declarations
PersistentSavedBarriers.lean 2 declarations
PerturbedBarrierData.lean 1 declarations
PhysicalCompactLength.lean 6 declarations
PhysicalDyadicLength.lean 12 declarations
PhysicalLengthCharacterization.lean 5 declarations
PhysicalLengthRestriction.lean 4 declarations
PhysicalPieceLength.lean 1 declarations
PhysicalSmallBarrier.lean 1 declarations
PhysicalTagPayment.lean 5 declarations
PhysicalTimeLength.lean 2 declarations
PositiveCountableWeights.lean 3 declarations
PositivePhysicalCost.lean 2 declarations
PotentialWeightedWitness.lean 1 declarations
PrincipalNormalization.lean 3 declarations
PriorBarrierConstruction.lean 1 declarations
PriorBarrierModulus.lean 1 declarations
PriorBarrierTrialMetric.lean 1 declarations
PriorityWeights.lean 11 declarations
ProtrusionBarrierObstruction.lean 4 declarations
RawArcPayment.lean 4 declarations
RawBarrierCompatibility.lean 2 declarations
RawGatedBarrier.lean 1 declarations
RayIndexOscillation.lean 4 declarations
RealAnchoredBarriers.lean 2 declarations
RealBandIntervalPayment.lean 1 declarations
RealBandPathPayment.lean 2 declarations
RealBandPhysicalPayment.lean 1 declarations
RealBarrierCollapse.lean 3 declarations
RealBarrierProjection.lean 3 declarations
RealBarrierSize.lean 2 declarations
RealBarrierTests.lean 11 declarations
RealBarrierVanishing.lean 1 declarations
RealSequencePayment.lean 3 declarations
RealSourceBarriers.lean 5 declarations
RectangleMeanOscillation.lean 1 declarations
RecursiveLimitBarriers.lean 2 declarations
RecursiveTailBudget.lean 1 declarations
RecursiveTestBudget.lean 8 declarations
RegularCurveNormalChart.lean 1 declarations
RegularCurveNormalStrip.lean 4 declarations
RegularJordanNormalBox.lean 2 declarations
RegularJordanNormalOrientation.lean 1 declarations
RegularJordanNormalSides.lean 2 declarations
ResidualIncidence.lean 5 declarations
RestrictedFragmentCosts.lean 3 declarations
RetaggedCost.lean 5 declarations
ReversedArclength.lean 4 declarations
ReversedPhysicalLength.lean 7 declarations
RotatedLocalizedPayment.lean 2 declarations
RotatedRealPayment.lean 4 declarations
SavedBarrierMargins.lean 2 declarations
SavedModelBarriers.lean 1 declarations
SelectableBarrierExclusion.lean 1 declarations
SelectableLevelBarrier.lean 1 declarations
SelectedBarrierRange.lean 1 declarations
SelectedBarrierTest.lean 1 declarations
SelectedNormalLimit.lean 1 declarations
SelectedRealBandNorm.lean 1 declarations
ShrinkingLengthFibers.lean 3 declarations
ShrinkingLocalWeightedCollars.lean 1 declarations
ShrinkingWeightedCollars.lean 1 declarations
SimpleArcLength.lean 2 declarations
SimpleArcPayment.lean 2 declarations
SmallMeanBudget.lean 5 declarations
SmallModelBarrier.lean 1 declarations
SmallWeightedArcs.lean 2 declarations
SourceStokesBudgetEstimate.lean 1 declarations
SphericalChartCost.lean 5 declarations
SphericalWeightedLength.lean 4 declarations
SquareQuarterOscillation.lean 2 declarations
StableBarrierContours.lean 1 declarations
StokesBudget.lean 2 declarations
StrongWeightedPullback.lean 1 declarations
TerminalCollarOscillation.lean 3 declarations
TerminalLimitPayment.lean 1 declarations
TerminalLinePayment.lean 1 declarations
TerminalNormBudget.lean 3 declarations
TerminalOscillation.lean 2 declarations
TerminalSourcePayment.lean 1 declarations
ThresholdImagePayment.lean 3 declarations
TimeIncidenceReparametrization.lean 5 declarations
TranslatedPhysicalBarrier.lean 4 declarations
TupleIncidence.lean 4 declarations
TwoEndedFragmentBudget.lean 1 declarations
UngatedBarrier.lean 2 declarations
UnitGraphCapacity.lean 1 declarations
VariableWeightedPullback.lean 1 declarations
VerticalCirclePayment.lean 3 declarations
VerticalLimitPayment.lean 1 declarations
VerticalTerminalPayment.lean 2 declarations
WeightedAnnularCollars.lean 2 declarations
WeightedCollarArcs.lean 2 declarations
WeightedCollarAvoidance.lean 3 declarations
WeightedCollarLevelTolls.lean 2 declarations
WeightedCollarLevels.lean 3 declarations
WeightedCollarNeighborhoods.lean 8 declarations
WeightedCollarTopology.lean 3 declarations
WeightedCurveLength.lean 3 declarations
WeightedHausdorffImage.lean 3 declarations
WeightedIntermediateCollar.lean 1 declarations
WeightedInversePieceCurve.lean 2 declarations
WeightedJordanCovers.lean 1 declarations
WeightedOneEndedLevelTolls.lean 1 declarations
WeightedOneEndedSplicing.lean 1 declarations
WeightedPhysicalChart.lean 6 declarations
WeightedPhysicalCollars.lean 1 declarations
WeightedScalarTests.lean 7 declarations
WeightedTwoEndedLevelTolls.lean 1 declarations
WeightedTwoEndedSplicing.lean 1 declarations