OAI/Analysis/CircleDomains/Rigidity/
656 declarations, 0 contain sorry, 0 declared as axioms; 227 files
Files
- ActualAxialCircleFlux.lean 1 declarations
- ActualAxialSlice.lean 1 declarations
- ActualEnclosedCircleSlice.lean 1 declarations
- ActualFiniteCircleFlux.lean 1 declarations
- ActualFiniteFluxLimit.lean 1 declarations
- ActualMaskedTransfer.lean 1 declarations
- AffineTracePairs.lean 2 declarations
- AssembledMaskedModel.lean 2 declarations
- AxialBandFlux.lean 4 declarations
- AxialChordGeometry.lean 7 declarations
- AxialChordInterior.lean 2 declarations
- AxialCircleFlux.lean 5 declarations
- AxialClosedDiskIntegral.lean 1 declarations
- AxialCommonPointTrace.lean 1 declarations
- AxialLineDifferentiation.lean 4 declarations
- AxialLineIntegral.lean 4 declarations
- AxialSlicesFromTrace.lean 1 declarations
- AxialSwapDisks.lean 4 declarations
- AxialTargetDiskMeasure.lean 4 declarations
- BoundaryTrace.lean 4 declarations
- CircleFluxStability.lean 3 declarations
- CircleProjectionFlux.lean 5 declarations
- CodeBranchFreeTrace.lean 1 declarations
- CodeFreeTrace.lean 1 declarations
- CodePeriodFreeTrace.lean 1 declarations
- CodeRealFreeTrace.lean 1 declarations
- CompactScalarAxialDerivative.lean 1 declarations
- ComponentTrace.lean 4 declarations
- ConditionalFiniteFlux.lean 1 declarations
- ConditionalNormalizedRigidity.lean 1 declarations
- ConditionalRigidity.lean 3 declarations
- ConductivityAlgebra.lean 6 declarations
- ConductivityCoefficient.lean 6 declarations
- ConductivityContraction.lean 12 declarations
- ConductivityDistortion.lean 2 declarations
- ConductivityEnergy.lean 2 declarations
- ConductivityEnergyBounds.lean 2 declarations
- ConductivityExterior.lean 3 declarations
- ConductivityFlux.lean 3 declarations
- ConductivityGlobalEnergy.lean 2 declarations
- ConductivityHeightCompactness.lean 1 declarations
- ConductivityHeightLimit.lean 1 declarations
- ConductivityJacobianBoundary.lean 2 declarations
- ConductivityJacobianLimit.lean 1 declarations
- ConductivityLocalEnergy.lean 1 declarations
- ConductivityWeakFields.lean 3 declarations
- ConjugateBeltramiL2.lean 10 declarations
- CorrespondenceMaskContinuity.lean 2 declarations
- CorrespondenceMaskPlateau.lean 1 declarations
- CountableAxialDiskTolls.lean 4 declarations
- CountableMaskedStages.lean 1 declarations
- CountableMatchedComponents.lean 11 declarations
- CountableTraceEnumeration.lean 7 declarations
- ENNRealBoundaryTrace.lean 2 declarations
- EnclosedCircleChords.lean 4 declarations
- EnclosedCrossingSum.lean 1 declarations
- EnclosedFluxIntegration.lean 2 declarations
- EventualFiniteFlux.lean 1 declarations
- ExactTraceFamily.lean 3 declarations
- ExactTraceSmoothing.lean 1 declarations
- ExactTraceSobolevError.lean 2 declarations
- ExactTraceTests.lean 3 declarations
- ExteriorMaskReplacement.lean 7 declarations
- FiniteCoreAnalyticTrace.lean 3 declarations
- FiniteInnerFluxLimit.lean 1 declarations
- FiniteMatchedField.lean 6 declarations
- FiniteTraceMask.lean 10 declarations
- FluxLimit.lean 2 declarations
- GapFluxTelescoping.lean 1 declarations
- GeometricRigidity.lean 3 declarations
- GlobalSmoothMatchedMasks.lean 1 declarations
- InnerPeriodMask.lean 1 declarations
- IntegrableAxialRestriction.lean 1 declarations
- IntervalTraceExtension.lean 2 declarations
- InwardMaskSelection.lean 3 declarations
- LipschitzTracePairs.lean 3 declarations
- LocalBandTagNullTrace.lean 1 declarations
- LocalMaskNeighborhoods.lean 2 declarations
- LocalTraceMaskSobolev.lean 1 declarations
- MaskAtlasGeometricAssembly.lean 1 declarations
- MaskAtlasGeometricCompletion.lean 1 declarations
- MaskBranchCollars.lean 3 declarations
- MaskIndependentMeanLowerBound.lean 2 declarations
- MaskTopology.lean 9 declarations
- MaskedCircleCost.lean 2 declarations
- MaskedCircleEnergy.lean 4 declarations
- MaskedCircleFillings.lean 5 declarations
- MaskedCircleMetric.lean 6 declarations
- MaskedCircuitLift.lean 1 declarations
- MaskedCofiniteMetric.lean 2 declarations
- MaskedCoordinateData.lean 1 declarations
- MaskedCoordinateModel.lean 1 declarations
- MaskedCoordinateStage.lean 2 declarations
- MaskedCoordinates.lean 3 declarations
- MaskedCorePreparation.lean 3 declarations
- MaskedFilledEnergy.lean 2 declarations
- MaskedFiniteTransfer.lean 1 declarations
- MaskedGridPreparation.lean 2 declarations
- MaskedGridSelection.lean 1 declarations
- MaskedLevelCompatibility.lean 2 declarations
- MaskedLevelData.lean 10 declarations
- MaskedLineNullImage.lean 1 declarations
- MaskedMetric.lean 3 declarations
- MaskedModelData.lean 1 declarations
- MaskedModelTerminalBranches.lean 1 declarations
- MaskedStageCollar.lean 1 declarations
- MaskedStageEnergy.lean 6 declarations
- MaskedStageSourceStokes.lean 1 declarations
- MaskedStageStokes.lean 1 declarations
- MaskedStageTerminalLifts.lean 2 declarations
- MaskedStokesApplication.lean 1 declarations
- MaskedStokesGeometry.lean 2 declarations
- MaskedTerminalBranches.lean 3 declarations
- MaskedTerminalLabel.lean 1 declarations
- MaskedTransferWithData.lean 1 declarations
- MaskedWedgeCost.lean 5 declarations
- MatchedCommonPoints.lean 4 declarations
- MatchedComponentSides.lean 2 declarations
- MatchedConformalEnds.lean 12 declarations
- MatchedDiskDomainGeometry.lean 3 declarations
- MatchedDiskNeighborhood.lean 1 declarations
- MatchedEndChains.lean 1 declarations
- MatchedEndsHomeomorph.lean 3 declarations
- MatchedImageCores.lean 4 declarations
- MatchedInnerCircleFlux.lean 3 declarations
- MatchedIntervalCoverage.lean 3 declarations
- MatchedMaskContinuity.lean 2 declarations
- MatchedMaskDomain.lean 1 declarations
- MatchedMaskGlobalSobolev.lean 1 declarations
- MatchedMaskLineNull.lean 1 declarations
- MatchedMaskSupport.lean 2 declarations
- MatchedPrincipalFlux.lean 1 declarations
- MatchedRealMaskConstruction.lean 1 declarations
- MatchedRealMaskData.lean 4 declarations
- MatchedRealMaskSobolev.lean 4 declarations
- MatchedResidualDust.lean 3 declarations
- MatchedRoundDisks.lean 4 declarations
- MatchedScalarIntervals.lean 16 declarations
- MatchedSliceCover.lean 1 declarations
- MatchedSliceEstimate.lean 1 declarations
- MatchedSourceProjection.lean 2 declarations
- MeanCircleLevelTrace.lean 1 declarations
- MeanCircleNullTrace.lean 1 declarations
- MeanIndexNullTrace.lean 1 declarations
- MeanMaskedPhysicalData.lean 1 declarations
- ModelCompactHeightTrace.lean 2 declarations
- ModelHeightTracePairs.lean 1 declarations
- ModelPointTrace.lean 4 declarations
- ModelSourceTracePairs.lean 3 declarations
- NonnegativeZeroTraceExtension.lean 3 declarations
- NormalizedRigidityFromTrace.lean 1 declarations
- OrderedMaskedSelection.lean 4 declarations
- PerturbedMeanFreeTrace.lean 2 declarations
- PhysicalMaskedBranches.lean 1 declarations
- PreparedMaskAtlasGeometry.lean 1 declarations
- PrincipalAbsentMaskedTransfer.lean 1 declarations
- PrincipalCircleFlux.lean 3 declarations
- PrincipalCircleFluxLimit.lean 3 declarations
- PrincipalMaskedTransfer.lean 1 declarations
- PrincipalOuterFlux.lean 3 declarations
- PrincipalPhysicalWitness.lean 5 declarations
- PrincipalRealBeltrami.lean 5 declarations
- PrincipalRealBeltramiProof.lean 1 declarations
- PrincipalRealTransfer.lean 1 declarations
- PrincipalScalarSolver.lean 3 declarations
- PrincipalScalarSolverProof.lean 2 declarations
- PriorityPointTrace.lean 4 declarations
- PriorityTracePairs.lean 2 declarations
- ProjectedZeroTrace.lean 1 declarations
- QuadrantFlux.lean 8 declarations
- QuarterFluxIntegrability.lean 1 declarations
- RankedCodeTraces.lean 5 declarations
- RawArcNullTrace.lean 1 declarations
- RawLevelNullTrace.lean 1 declarations
- RealBandTagNullTrace.lean 1 declarations
- RealBeltramiCoefficientReduction.lean 6 declarations
- RealBeltramiL2Reduction.lean 5 declarations
- RealCapMaskNeighborhoods.lean 2 declarations
- RegularMaskedStokes.lean 3 declarations
- RemovabilityMobiusTransport.lean 3 declarations
- RemovableAreaZero.lean 3 declarations
- RemovableNormalizedExtension.lean 2 declarations
- RigidityNormalizationReduction.lean 1 declarations
- SamplingTraceContinuity.lean 2 declarations
- ScalarModelConductivity.lean 5 declarations
- SeededMaskedSelection.lean 3 declarations
- SelectableMaskedCoordinate.lean 12 declarations
- SelectedTraceBound.lean 2 declarations
- SignedTraceTruncation.lean 9 declarations
- SignedTraceTruncationWeak.lean 1 declarations
- SmoothCommonPointTrace.lean 1 declarations
- SmoothMatchedScalar.lean 2 declarations
- SmoothReplacementFlux.lean 1 declarations
- SmoothTraceTruncation.lean 11 declarations
- SphereTracePairNull.lean 3 declarations
- SubordinateMaskedBranches.lean 1 declarations
- TaggedNullTrace.lean 2 declarations
- TraceBalloonCutoff.lean 1 declarations
- TraceBalloonDensity.lean 1 declarations
- TraceBalloonPacking.lean 4 declarations
- TraceBalloonRadii.lean 12 declarations
- TraceBalloonRealCoordinates.lean 1 declarations
- TraceBalloonSystem.lean 4 declarations
- TraceBandLevel.lean 1 declarations
- TraceCompression.lean 9 declarations
- TraceCompressionPayment.lean 3 declarations
- TraceEnumerationUnion.lean 1 declarations
- TraceIntegralNull.lean 2 declarations
- TraceIntervalPayment.lean 3 declarations
- TraceLineTails.lean 6 declarations
- TraceMaskAEPayment.lean 3 declarations
- TraceMaskLinePayment.lean 5 declarations
- TraceMaskOpenSobolev.lean 1 declarations
- TraceMaskPlateauSobolev.lean 2 declarations
- TraceMaskPrimitive.lean 9 declarations
- TraceMaskRectangle.lean 2 declarations
- TraceMaskTail.lean 5 declarations
- TracePrimitiveContinuity.lean 2 declarations
- TracePrimitiveMeasurability.lean 6 declarations
- TracePrimitivePlateau.lean 5 declarations
- TraceTruncationLimits.lean 2 declarations
- TraceTruncationWeak.lean 1 declarations
- TypicalAxialDiskTolls.lean 2 declarations
- UniformizedMaskedTransfer.lean 1 declarations
- ZeroTraceConformalTransport.lean 1 declarations
- ZeroTraceEnergy.lean 3 declarations
- ZeroTraceExtension.lean 3 declarations