OAI/MeasureTheory/Falconer/Graphs/
709 declarations, 0 contain sorry, 0 declared as axioms; 181 files
Files
- ActualDirectGraph.lean 1 declarations
- ActualDistanceChildEnergy.lean 1 declarations
- ActualDistanceDegrees.lean 2 declarations
- ActualDistanceGraphAssembly.lean 3 declarations
- ActualDistanceHFGraph.lean 2 declarations
- ActualProductChildEnergy.lean 1 declarations
- ActualProductDegrees.lean 5 declarations
- ActualProductEnergyFinite.lean 3 declarations
- ActualProductGraphAssembly.lean 3 declarations
- AllDimensionalGraphGeometry.lean 10 declarations
- BipartitePivot.lean 7 declarations
- CommonRowNormalization.lean 12 declarations
- CoordinateGraph.lean 5 declarations
- CoordinateGraphObstruction.lean 1 declarations
- DenseGraphComparableParameters.lean 1 declarations
- DenseGraphObstruction.lean 1 declarations
- DenseGraphParameters.lean 1 declarations
- DenseGraphRadiusObstruction.lean 1 declarations
- DenseUnbalancedGraph.lean 1 declarations
- DescriptorGraph.lean 3 declarations
- DescriptorProductGraph.lean 1 declarations
- DistanceGraphCross.lean 2 declarations
- DistanceGraphIntegral.lean 1 declarations
- DistanceGraphPointwise.lean 1 declarations
- DistancePairDegree.lean 6 declarations
- DistanceSupportedGraph.lean 4 declarations
- DyadicGraph.lean 6 declarations
- DyadicRowCount.lean 2 declarations
- EligibleDistanceGraphSum.lean 4 declarations
- EligibleDyadicGraph.lean 7 declarations
- EligibleProductGraphSum.lean 9 declarations
- Energy.lean 12 declarations
- FiberEnergy.lean 5 declarations
- FiberPairing.lean 6 declarations
- FiberSlice.lean 6 declarations
- FiberTrace.lean 4 declarations
- FinsetSchur.lean 1 declarations
- FlexibleGraphChild.lean 2 declarations
- GraphActualMixedDerivatives.lean 3 declarations
- GraphActualNonedgeGeometry.lean 4 declarations
- GraphActualNonedgeSum.lean 2 declarations
- GraphActualQuadCells.lean 6 declarations
- GraphActualTransport.lean 5 declarations
- GraphAlgebraicDirections.lean 8 declarations
- GraphAmplitudeDerivatives.lean 4 declarations
- GraphAmplitudeRepresentative.lean 10 declarations
- GraphAmplitudeScale.lean 6 declarations
- GraphAmplitudeSupport.lean 7 declarations
- GraphBallCover.lean 3 declarations
- GraphBinDerivatives.lean 1 declarations
- GraphCartesianSubstitution.lean 6 declarations
- GraphChartIntegral.lean 5 declarations
- GraphChartRegularity.lean 5 declarations
- GraphChartVariation.lean 6 declarations
- GraphCompleteWeightSupport.lean 8 declarations
- GraphConeCutoff.lean 6 declarations
- GraphCoordinateInverse.lean 9 declarations
- GraphDegrees.lean 8 declarations
- GraphDensity.lean 2 declarations
- GraphDensityRadius.lean 2 declarations
- GraphDerivativeBounds.lean 7 declarations
- GraphDirectionStability.lean 4 declarations
- GraphEndpointContinuity.lean 13 declarations
- GraphEnergyError.lean 1 declarations
- GraphEnergyEstimate.lean 2 declarations
- GraphErrorAbsorption.lean 1 declarations
- GraphEtaIntegratedNonedge.lean 2 declarations
- GraphEtaNonstationary.lean 3 declarations
- GraphFiberPacking.lean 6 declarations
- GraphFixedCutoffs.lean 11 declarations
- GraphFourMassBound.lean 3 declarations
- GraphFourTransformExpansion.lean 4 declarations
- GraphFourTransformPointIntegral.lean 2 declarations
- GraphGeometry.lean 12 declarations
- GraphGlobalBump.lean 2 declarations
- GraphGlobalChart.lean 6 declarations
- GraphGlobalDomain.lean 7 declarations
- GraphGlobalPhase.lean 9 declarations
- GraphGlobalSupports.lean 9 declarations
- GraphInheritedNonedge.lean 1 declarations
- GraphInheritedNonedgePower.lean 1 declarations
- GraphInheritedTransformChart.lean 2 declarations
- GraphLiftInverse.lean 8 declarations
- GraphLiftJacobian.lean 8 declarations
- GraphMixedComposition.lean 3 declarations
- GraphNonedgeAmplitude.lean 2 declarations
- GraphNonedgeErrorScale.lean 1 declarations
- GraphNonedgeFiniteSum.lean 2 declarations
- GraphNonedgeGradient.lean 5 declarations
- GraphNonedgeIndexCount.lean 9 declarations
- GraphNonedgeIntegralErrors.lean 3 declarations
- GraphNonedgePerturbation.lean 10 declarations
- GraphNormalization.lean 5 declarations
- GraphOriginalFubini.lean 6 declarations
- GraphOriginalGraphRemoval.lean 1 declarations
- GraphOriginalNonedgePower.lean 2 declarations
- GraphParentDiameter.lean 4 declarations
- GraphPointIntegralChart.lean 2 declarations
- GraphPolarAnnulus.lean 7 declarations
- GraphPolarJacobian.lean 10 declarations
- GraphPolicyScales.lean 8 declarations
- GraphProductMeasure.lean 5 declarations
- GraphProfileCoefficient.lean 3 declarations
- GraphReferenceZoom.lean 1 declarations
- GraphRetainedEdges.lean 6 declarations
- GraphScalarRegularity.lean 1 declarations
- GraphScaleData.lean 3 declarations
- GraphScaleDirection.lean 1 declarations
- GraphSchur.lean 4 declarations
- GraphSignChart.lean 4 declarations
- GraphSignPartition.lean 10 declarations
- GraphSignSupports.lean 6 declarations
- GraphSliceDerivatives.lean 3 declarations
- GraphSpatialFubini.lean 4 declarations
- GraphTestScales.lean 1 declarations
- GraphTorusArcLength.lean 5 declarations
- GraphTransformChart.lean 1 declarations
- GraphTransportIntegrability.lean 9 declarations
- GraphTwoErrors.lean 1 declarations
- GraphWeightDerivatives.lean 8 declarations
- GraphZIntegratedNonedge.lean 2 declarations
- GraphZNonedgeScale.lean 1 declarations
- GraphZNonstationary.lean 2 declarations
- JetStateGraph.lean 9 declarations
- LocalDistanceCollision.lean 1 declarations
- NearGraph.lean 5 declarations
- OuterGraphData.lean 1 declarations
- OuterGraphStep.lean 2 declarations
- OuterRootGraphBound.lean 1 declarations
- PairCollisionTonelli.lean 2 declarations
- ParentAbsoluteGraphAssembly.lean 4 declarations
- ParentGraphEnergy.lean 3 declarations
- ParentGraphIndices.lean 7 declarations
- ParentRetainedEnergy.lean 8 declarations
- PlanarGraphBudgetApplication.lean 1 declarations
- PolicyGraphAt.lean 1 declarations
- PolicyGraphAtRecurrence.lean 1 declarations
- PolicyGraphAtStep.lean 1 declarations
- PolicyGraphData.lean 1 declarations
- PolicyGraphError.lean 3 declarations
- PolicyGraphGeometry.lean 3 declarations
- PolicyGraphRecurrence.lean 2 declarations
- PolicyGraphStep.lean 3 declarations
- PrefixGraphSpecialization.lean 2 declarations
- PrefixSuccessorEnergy.lean 8 declarations
- ProductAbsoluteGraphAssembly.lean 3 declarations
- ProductEnergyMaximum.lean 7 declarations
- ProductEnergyTransfer.lean 2 declarations
- ProductGraphEnergy.lean 2 declarations
- ProductGraphIndices.lean 7 declarations
- ProductGraphIntegral.lean 1 declarations
- ProductGraphPointwise.lean 1 declarations
- ProductPairDegree.lean 4 declarations
- ProfileGraph.lean 3 declarations
- ProfileGraphBudget.lean 2 declarations
- ProfileGraphDegree.lean 3 declarations
- ProfileGraphError.lean 1 declarations
- ProfileGraphEstimate.lean 1 declarations
- RecursiveEnergyFamily.lean 7 declarations
- RegularGraphCosts.lean 3 declarations
- RegularGraphObstruction.lean 1 declarations
- RegularGraphRadiusCosts.lean 1 declarations
- RegularGraphRadiusObstruction.lean 1 declarations
- RegularUnbalancedGraph.lean 1 declarations
- RootParentEnergy.lean 3 declarations
- RoundedGraphCounts.lean 3 declarations
- RoundedGraphData.lean 2 declarations
- RoundedProjectionGraph.lean 3 declarations
- ScalarDenseGraph.lean 1 declarations
- ScalarGraphCoding.lean 2 declarations
- SmoothFiberEstimate.lean 2 declarations
- SourceSpatialEnergy.lean 7 declarations
- TwoGraphChildren.lean 5 declarations
- TwoGraphScales.lean 2 declarations
- TwoProfileGraph.lean 4 declarations
- UniformDistancePairDegree.lean 1 declarations
- WeakGraphObstruction.lean 1 declarations
- WeakGraphRadiusObstruction.lean 1 declarations
- WeakUnbalancedGraph.lean 1 declarations
- WeightedDistanceCoincidence.lean 4 declarations
- WitnessGraph.lean 3 declarations