OAI/Geometry/IsometricImmersion/Pulses/
271 declarations, 0 contain sorry, 0 declared as axioms; 37 files
Files
- ActualClassQForcingMoment.lean 1 declarations
- ActualForcingCoefficient.lean 6 declarations
- ActualForcingMoment.lean 3 declarations
- ActualPulseMetricCloseness.lean 3 declarations
- ActualQPulseForcing.lean 2 declarations
- ActualQPulseForcingGlobal.lean 1 declarations
- ActualTwoSidedPulseSeparation.lean 2 declarations
- CutoffEdgeMoment.lean 10 declarations
- FiniteOscillatoryMoment.lean 4 declarations
- ForcingCoefficientSign.lean 6 declarations
- OffPulseMetricBounds.lean 3 declarations
- OriginalPulseExclusion.lean 1 declarations
- PulseActualDensity.lean 2 declarations
- PulseCurvaturePrincipal.lean 14 declarations
- PulseDensityGlobal.lean 2 declarations
- PulseDensitySlab.lean 7 declarations
- PulseDerivativeBounds.lean 28 declarations
- PulseEdgeReferenceDistance.lean 4 declarations
- PulseFirstJetControl.lean 12 declarations
- PulseFlowDistance.lean 5 declarations
- PulseMoment.lean 10 declarations
- PulseMomentError.lean 8 declarations
- PulseMomentGeometry.lean 19 declarations
- PulseNeighborhood.lean 5 declarations
- PulseNeighborhoodAdapters.lean 4 declarations
- PulseOperatorMoment.lean 5 declarations
- PulseProfiles.lean 41 declarations
- PulseScalarContradiction.lean 2 declarations
- PulseSecondXi.lean 11 declarations
- PulseSpatialParts.lean 9 declarations
- PulseTemporalMoment.lean 5 declarations
- PulseTemporalParts.lean 5 declarations
- PulseTestEnergy.lean 12 declarations
- QPulseFirstJetBudget.lean 5 declarations
- QReferenceForcingMargins.lean 2 declarations
- ReferencePulseEdgeInitial.lean 1 declarations
- ShearedPulseRegions.lean 11 declarations