OAI/Analysis/CircleDomains/Transfer/
439 declarations, 0 contain sorry, 0 declared as axioms; 126 files
Files
- ActualMixedTransfer.lean 1 declarations
- AnchoredMeanSourceBound.lean 1 declarations
- AssembledMixedModel.lean 1 declarations
- AssembledRealTransfer.lean 1 declarations
- BoundedScalarFillings.lean 11 declarations
- ChartFiberConcentration.lean 2 declarations
- CofiniteTransfer.lean 4 declarations
- CompletedChart.lean 8 declarations
- ComplexC1LevelChart.lean 1 declarations
- ComplexHausdorffTransport.lean 4 declarations
- ComplexSourceWitness.lean 1 declarations
- ContinuousSourceProjection.lean 1 declarations
- CoreCrossing.lean 4 declarations
- CoreGeometry.lean 12 declarations
- CountableRealTransfer.lean 5 declarations
- EmptyDustScalarModel.lean 1 declarations
- EnlargedRealModels.lean 2 declarations
- ExteriorImageCircuit.lean 1 declarations
- FilledCoordinates.lean 10 declarations
- FilledGapIntegration.lean 2 declarations
- FilledMetric.lean 5 declarations
- FilledScalarLineData.lean 4 declarations
- FiniteChartConnectivity.lean 6 declarations
- FiniteHoleCore.lean 3 declarations
- FiniteMixedModel.lean 1 declarations
- FiniteRealChartIntersections.lean 2 declarations
- GeometricCompletion.lean 1 declarations
- GeometricGridAssembly.lean 2 declarations
- GlobalCoreExtension.lean 5 declarations
- GraphGeometricCompletion.lean 1 declarations
- GraphGridCells.lean 10 declarations
- GraphGridCompatibility.lean 4 declarations
- GridCollisionEstimate.lean 4 declarations
- GridCollisions.lean 9 declarations
- GridCompatibility.lean 5 declarations
- GridCoordinateFilling.lean 4 declarations
- GridFamilies.lean 2 declarations
- GridObstacles.lean 2 declarations
- GridPreparation.lean 3 declarations
- GridSelection.lean 2 declarations
- GridStageContours.lean 1 declarations
- GridSummability.lean 4 declarations
- GridWidthSelection.lean 2 declarations
- LevelChartBox.lean 2 declarations
- LevelChartJacobian.lean 1 declarations
- LogarithmicCutCharts.lean 7 declarations
- MarkedModelTerminalControl.lean 1 declarations
- MixedCoordinateModel.lean 1 declarations
- MixedMarkedModels.lean 6 declarations
- ModelAppendedPairs.lean 3 declarations
- ModelAppendedTests.lean 1 declarations
- ModelExteriorEstimate.lean 1 declarations
- ModelFixedWorkingBounds.lean 2 declarations
- ModelFlattenedSelection.lean 2 declarations
- ModelHeightDescent.lean 6 declarations
- ModelHeightErrorTransport.lean 1 declarations
- ModelHeightSourceError.lean 2 declarations
- ModelHeightWorkingError.lean 2 declarations
- ModelHorizontalApproximation.lean 1 declarations
- ModelLocalizedSelection.lean 1 declarations
- ModelPairWorkingError.lean 2 declarations
- ModelPriorityContinuity.lean 1 declarations
- ModelPriorityData.lean 1 declarations
- ModelPriorityPairs.lean 1 declarations
- ModelPrioritySupport.lean 1 declarations
- ModelProjectionFibers.lean 3 declarations
- ModelRealSubfamily.lean 1 declarations
- ModelRealTerminals.lean 2 declarations
- ModelScalarDescent.lean 2 declarations
- ModelScalarPullback.lean 2 declarations
- ModelSelectedBounds.lean 5 declarations
- ModelSelectedSupport.lean 1 declarations
- ModelSelectedTests.lean 1 declarations
- ModelWorkingCoordinates.lean 2 declarations
- NonpointModelEnds.lean 3 declarations
- OrderedGridCompatibility.lean 1 declarations
- PeriodicFilling.lean 44 declarations
- PointDustModels.lean 4 declarations
- PotentialPrescribedChartBound.lean 1 declarations
- PrincipalAbsentMixedTransfer.lean 1 declarations
- PrincipalMixedTransfer.lean 1 declarations
- PrincipalSubordinateGraphTransfer.lean 1 declarations
- PrincipalSubordinateMixedTransfer.lean 1 declarations
- RadialShrinkImages.lean 2 declarations
- RankOneFilling.lean 3 declarations
- RealEndCorrespondence.lean 2 declarations
- RealGridTransfer.lean 1 declarations
- RealMarkedModels.lean 10 declarations
- RealPresentationTransfer.lean 5 declarations
- RealTargetEnds.lean 12 declarations
- RealTransferStage.lean 2 declarations
- ReciprocalGridSelection.lean 8 declarations
- RegularC1Chart.lean 1 declarations
- RegularCore.lean 4 declarations
- RegularImageCircuit.lean 1 declarations
- ResidualImage.lean 8 declarations
- RetainedOriginalTest.lean 2 declarations
- RetainedRegionAvoidance.lean 3 declarations
- RetainedScalarEstimates.lean 7 declarations
- RetainedScalarTails.lean 9 declarations
- RetainedSmallTests.lean 1 declarations
- RetainedTerminalGeometry.lean 2 declarations
- RetainedTestCrossings.lean 2 declarations
- RoundOuterCore.lean 7 declarations
- ScalarHoleFillings.lean 5 declarations
- ScalarImageIdentification.lean 3 declarations
- ScalarModelLinearRecovery.lean 2 declarations
- ScalarModelPostcomposition.lean 5 declarations
- SelectedMixedModels.lean 2 declarations
- ShrinkingRealModels.lean 8 declarations
- SmallImageDustContours.lean 1 declarations
- SourceAnchor.lean 4 declarations
- SourceEndProjection.lean 7 declarations
- SourceStokesEventual.lean 1 declarations
- SourceStokesExclusion.lean 1 declarations
- SourceTargetEnds.lean 6 declarations
- SubordinateGraphCompletion.lean 1 declarations
- SubordinateGraphFilling.lean 1 declarations
- SubordinateGridStage.lean 1 declarations
- TerminalTransfer.lean 4 declarations
- TransportedMeanIndex.lean 1 declarations
- TransportedRealCoordinates.lean 3 declarations
- TransportedRealLocalization.lean 2 declarations
- TransportedTerminalBranches.lean 9 declarations
- VerticalFilledJump.lean 1 declarations
- VerticalRetainedCrossings.lean 2 declarations