OAI/Analysis/LipschitzHilbert/Estimates/

Files

• ActualBinPairing.lean 2 declarations
• ActualBinReconstruction.lean 1 declarations
• ActualErrorSource.lean 7 declarations
• AdmissibleListCount.lean 1 declarations
• AllDyadicWeakL1.lean 4 declarations
• AmplitudeAllWeights.lean 2 declarations
• AmplitudeApproximation.lean 8 declarations
• AmplitudeApproximationL1.lean 8 declarations
• AmplitudeClassBound.lean 1 declarations
• AmplitudeClassCount.lean 2 declarations
• AmplitudeClassSum.lean 2 declarations
• AmplitudeDiscardedSum.lean 1 declarations
• AmplitudeDisparity.lean 3 declarations
• AmplitudeEnergy.lean 5 declarations
• AmplitudeErrorDecay.lean 2 declarations
• AmplitudeLevelL1.lean 2 declarations
• AmplitudeLp.lean 4 declarations
• AmplitudeMatrixBound.lean 2 declarations
• AmplitudeMatrixNormalization.lean 1 declarations
• AmplitudeNormalizedEnergy.lean 3 declarations
• AmplitudeRetainedDecay.lean 2 declarations
• AmplitudeRetainedSum.lean 2 declarations
• AmplitudeTailCost.lean 4 declarations
• AmplitudeTailParameters.lean 1 declarations
• AveragedSquareMoment.lean 2 declarations
• BinCarleson.lean 3 declarations
• BinErrorParameters.lean 1 declarations
• BinaryDensityBound.lean 2 declarations
• BoundedDuality.lean 6 declarations
• BoundedProjectedOutput.lean 2 declarations
• BoundedSupportedCoordinates.lean 1 declarations
• BoxPolynomialWeight.lean 3 declarations
• BoxSynthesisEnergy.lean 1 declarations
• BoxVariationWeights.lean 6 declarations
• CarlesonExponential.lean 3 declarations
• CarlesonProductEnergy.lean 2 declarations
• CarlesonSorting.lean 2 declarations
• CarrierSlopeMotion.lean 3 declarations
• ChartPullback.lean 10 declarations
• ClippedAverage.lean 1 declarations
• ClippedSlopeBox.lean 8 declarations
• CoefficientDecomposition.lean 3 declarations
• CoefficientPolarization.lean 1 declarations
• ColoredPlanarEnergy.lean 2 declarations
• CompactCompositionCommutator.lean 3 declarations
• CompactMollification.lean 4 declarations
• CompactMollificationFamily.lean 5 declarations
• CompactMollificationL2.lean 2 declarations
• CompactMollificationSupport.lean 2 declarations
• CompactWitness.lean 2 declarations
• ComparableCommutatorSum.lean 5 declarations
• ComparableDerivativeSum.lean 2 declarations
• ComparableDerivativeSupport.lean 3 declarations
• ComparableSelectedSlab.lean 1 declarations
• ComplexVariation.lean 5 declarations
• ComplexVariationCoordinates.lean 2 declarations
• ConditionalSlopeOperator.lean 3 declarations
• ConditionalSlopePrincipalValue.lean 3 declarations
• ConditionalUniformTruncation.lean 1 declarations
• ConditionalVariableEndpoints.lean 1 declarations
• ConstructedCovariantTop.lean 1 declarations
• ConstructedGlobalNeighborhood.lean 1 declarations
• ConstructedSynthesisNeighborhood.lean 1 declarations
• ConstructedTopFamily.lean 1 declarations
• ConstructedTopNeighborhood.lean 1 declarations
• ContinuousBMOMoments.lean 1 declarations
• ContinuousBMOTail.lean 2 declarations
• CountGeometryParameters.lean 2 declarations
• CountParameters.lean 6 declarations
• CountThreshold.lean 1 declarations
• CountableCarleson.lean 10 declarations
• CountingDiscard.lean 4 declarations
• CubicDualityEstimate.lean 1 declarations
• DampedSimplexBounds.lean 3 declarations
• DisjointIntervalVariation.lean 1 declarations
• DyadicErrorProfile.lean 3 declarations
• DyadicErrorSource.lean 4 declarations
• DyadicLongScales.lean 2 declarations
• DyadicMeasureClass.lean 2 declarations
• DyadicSmoothEmbedding.lean 1 declarations
• DyadicSquareWeakL1.lean 10 declarations
• DyadicWeakL1.lean 3 declarations
• EndpointWeightBounds.lean 2 declarations
• EnvelopeDerivative.lean 2 declarations
• EnvelopeSynthesis.lean 6 declarations
• ErrorSourceBridge.lean 4 declarations
• ErrorSynthesisVariation.lean 4 declarations
• ExponentialThreshold.lean 5 declarations
• ExponentialVariation.lean 4 declarations
• FatTopTail.lean 1 declarations
• FiniteAmplitudeGeometric.lean 2 declarations
• FiniteBinCommutator.lean 2 declarations
• FiniteCarlesonEmbedding.lean 2 declarations
• FiniteClassRegroup.lean 2 declarations
• FiniteCommutatorSquare.lean 5 declarations
• FiniteEnergySchur.lean 3 declarations
• FiniteLogAmplitudeSum.lean 1 declarations
• FiniteMatrixDiscard.lean 2 declarations
• FiniteMeasureLepingle.lean 2 declarations
• FiniteMultiplierRecombination.lean 2 declarations
• FiniteNarrowPartition.lean 7 declarations
• FiniteRemovalIteration.lean 3 declarations
• FiniteRestrictedStrong.lean 3 declarations
• FiniteRestrictedStrongNull.lean 1 declarations
• FiniteSchur.lean 1 declarations
• FiniteSignedEnergy.lean 3 declarations
• FiniteSignedFunctions.lean 6 declarations
• FiniteSlopeGeometry.lean 2 declarations
• FiniteSmoothProduct.lean 1 declarations
• FiniteUnitAverage.lean 1 declarations
• FiniteUnitAverageL1.lean 1 declarations
• FiniteVariation.lean 6 declarations
• FirstArrival.lean 6 declarations
• FirstExceed.lean 8 declarations
• FrozenSlopeMultiplier.lean 3 declarations
• GeometricScaleWeights.lean 6 declarations
• GeometricTailExponential.lean 1 declarations
• GeometricTailMoments.lean 1 declarations
• GlobalExceptionalArea.lean 2 declarations
• GlobalLocalNeighborhood.lean 1 declarations
• GlobalNeighborhood.lean 1 declarations
• GlobalTopBoxes.lean 2 declarations
• HalfPowerDualTest.lean 9 declarations
• HardyPairL4.lean 4 declarations
• Hellinger.lean 6 declarations
• HilbertArbitraryEndpoint.lean 2 declarations
• HilbertEndpointCases.lean 2 declarations
• HilbertFiniteFourth.lean 1 declarations
• HilbertFiniteL2.lean 3 declarations
• HilbertSharpPairing.lean 1 declarations
• HilbertSignFourth.lean 1 declarations
• HilbertTimeDecomposition.lean 4 declarations
• HilbertTimeProfile.lean 7 declarations
• HilbertVariation.lean 2 declarations
• HorizontalDilation.lean 8 declarations
• HorizontalHilbertLp.lean 4 declarations
• HorizontalHilbertPairing.lean 3 declarations
• HorizontalHilbertProof.lean 1 declarations
• IntGeometricSum.lean 3 declarations
• IntegerSlopeMultiplicity.lean 3 declarations
• IntegralMinkowski.lean 2 declarations
• IntervalOscillation.lean 5 declarations
• IntervalPoincare.lean 6 declarations
• IntervalPolarization.lean 4 declarations
• IntervalSegmentCharging.lean 2 declarations
• JointLatticeAverage.lean 2 declarations
• L1MultiplierDominatedLimit.lean 3 declarations
• L2Conjugation.lean 6 declarations
• L2Indicator.lean 6 declarations
• L2IndicatorAlgebra.lean 3 declarations
• L2SpatialPartition.lean 3 declarations
• LaminarCarleson.lean 8 declarations
• LaminarChains.lean 9 declarations
• LaminarWeakL1.lean 3 declarations
• LayerEnergyMoments.lean 5 declarations
• LepingleIntervals.lean 2 declarations
• LepingleProof.lean 4 declarations
• LipschitzCompositionCommutator.lean 1 declarations
• LocalSelectedWidths.lean 1 declarations
• LocalizedEnvelope.lean 2 declarations
• LocalizedMihlinProfile.lean 15 declarations
• LocalizedSelectorDerivative.lean 6 declarations
• LocalizedSubbandOperator.lean 4 declarations
• LogEnergy.lean 12 declarations
• LogEnergyGradient.lean 14 declarations
• LongDyadicSum.lean 1 declarations
• LongHilbertPairing.lean 2 declarations
• LongScaleVariation.lean 3 declarations
• MarkedCost.lean 2 declarations
• MarkedShells.lean 5 declarations
• MartingaleExitTimes.lean 13 declarations
• MartingaleGeometricTail.lean 2 declarations
• MartingaleGoodLambda.lean 2 declarations
• MartingaleLocalMaximal.lean 6 declarations
• MartingaleMaximalL2.lean 5 declarations
• MaskComparison.lean 2 declarations
• MaskIntegral.lean 1 declarations
• MaskNormalization.lean 2 declarations
• MaskParameters.lean 4 declarations
• MaximalContainmentExclusion.lean 3 declarations
• MaximalL2Energy.lean 2 declarations
• MeanOscillation.lean 5 declarations
• MeasureClassLog.lean 2 declarations
• MihlinPVCommutator.lean 2 declarations
• MihlinTimeCommutator.lean 3 declarations
• MixedNorms.lean 2 declarations
• MixedTopTail.lean 1 declarations
• MomentSuperlevel.lean 3 declarations
• MonotoneCoefficientSum.lean 1 declarations
• MovingExponentialWeights.lean 6 declarations
• MovingSegmentLogs.lean 7 declarations
• MovingSegmentWeights.lean 2 declarations
• MovingWeightBudget.lean 3 declarations
• MultiplierError.lean 2 declarations
• NarrowPartitionBound.lean 4 declarations
• NarrowPartitionReconstruction.lean 3 declarations
• NarrowWindowNeighborhood.lean 3 declarations
• NeighborhoodEnergy.lean 2 declarations
• NeighborhoodExceptional.lean 3 declarations
• NeighborhoodGeometric.lean 2 declarations
• NestedAverage.lean 10 declarations
• NestedPerturbation.lean 2 declarations
• NormalizedLatticeAverage.lean 1 declarations
• NormalizedLatticeSpectrum.lean 2 declarations
• NormalizedProfileBudget.lean 3 declarations
• OperatorConjugation.lean 3 declarations
• OrderDistribution.lean 4 declarations
• OrdinaryModelConstruction.lean 2 declarations
• OrdinaryModelConstructionCost.lean 4 declarations
• OrdinaryModelNumerics.lean 2 declarations
• OriginalRecovery.lean 5 declarations
• ParityPartialSums.lean 5 declarations
• PartitionIntegral.lean 1 declarations
• PerturbedLepingle.lean 3 declarations
• PhysicalBinAdjoint.lean 1 declarations
• PlanarChangeVariables.lean 3 declarations
• PlanarCoefficientBudget.lean 1 declarations
• PlanarCoefficientNorm.lean 6 declarations
• PlanarColoredVectorEnergy.lean 1 declarations
• PlanarFixedScaleEnergy.lean 6 declarations
• PlanarHorizontalRescale.lean 7 declarations
• PlanarPairingEnergy.lean 2 declarations
• PlanarProfileBounds.lean 12 declarations
• PlanarProfilePolarization.lean 8 declarations
• PlanarSeparatedEnergy.lean 4 declarations
• PlaneCoordinates.lean 5 declarations
• PlaneSlopeLipschitz.lean 2 declarations
• PolynomialEnvelope.lean 10 declarations
• PolynomialLocalization.lean 16 declarations
• PolynomialMomentBound.lean 5 declarations
• PopularCountDiscard.lean 1 declarations
• PopularGroups.lean 3 declarations
• PopularTopCount.lean 1 declarations
• PopularTopCountPowers.lean 1 declarations
• PopularTopMask.lean 1 declarations
• PositiveAuxiliaryAverages.lean 3 declarations
• PositiveErrorMajorant.lean 21 declarations
• PrincipalTimeMoment.lean 3 declarations
• PrincipalValueProfileCommutator.lean 3 declarations
• ProductPVContinuity.lean 4 declarations
• ProductPVPointwiseBound.lean 5 declarations
• ProductPerturbation.lean 4 declarations
• ProductSlopePVTruncation.lean 3 declarations
• ProductSlopePrincipalValue.lean 7 declarations
• ProductSlopePrincipalValueBound.lean 7 declarations
• PublishedHilbertInput.lean 2 declarations
• PublishedInputs.lean 17 declarations
• RadialShrink.lean 14 declarations
• RankedMaximal.lean 5 declarations
• RawBMOMoments.lean 1 declarations
• RealFiniteVariation.lean 8 declarations
• ReferenceAnalysis.lean 7 declarations
• ReferenceCarleson.lean 1 declarations
• ReferenceChart.lean 7 declarations
• ReferenceException.lean 4 declarations
• ReferenceFamilyException.lean 7 declarations
• ReferenceSynthesis.lean 7 declarations
• ReferenceSynthesisL1.lean 1 declarations
• RelativeExitEnergy.lean 15 declarations
• RelativeExitIntervals.lean 3 declarations
• RelativeExitScales.lean 6 declarations
• RelativeMartingaleExits.lean 18 declarations
• RelativePartitionVariation.lean 1 declarations
• RestrictedLogDensity.lean 3 declarations
• RestrictedLogNumerics.lean 3 declarations
• RestrictedStrongForm.lean 7 declarations
• RestrictedStrongLp.lean 1 declarations
• RestrictedStrongOperator.lean 6 declarations
• RestrictedTestApproximation.lean 5 declarations
• RestrictedTestOpenApproximation.lean 3 declarations
• RestrictedTopWeakTwo.lean 1 declarations
• RetainedAmplitudeMatrix.lean 2 declarations
• RootTailGluing.lean 7 declarations
• ScalarRestrictedStrong.lean 8 declarations
• ScaledUnitSelector.lean 5 declarations
• ScaledWindowSpectrum.lean 6 declarations
• SectionMeasure.lean 1 declarations
• SegmentAmplitudes.lean 2 declarations
• SegmentCharging.lean 2 declarations
• SegmentWeights.lean 10 declarations
• SelectedCoefficientDerivative.lean 3 declarations
• SelectedScaleDerivative.lean 3 declarations
• SelectedTopInterval.lean 1 declarations
• SelfEnergy.lean 1 declarations
• SeparatedPlanarSynthesis.lean 2 declarations
• SeparatedSampling.lean 2 declarations
• SeparatedWitnessCount.lean 1 declarations
• SequenceExponents.lean 13 declarations
• SequenceNorms.lean 9 declarations
• SharpHilbertFourth.lean 1 declarations
• SharpHilbertL2.lean 2 declarations
• SharpHilbertThird.lean 2 declarations
• SharpHilbertThreeHalves.lean 2 declarations
• SharpRemainderDecay.lean 5 declarations
• SharpTimeMoment.lean 2 declarations
• SharpTimeParameters.lean 7 declarations
• SharpTimeSplit.lean 2 declarations
• ShearedEnvelope.lean 2 declarations
• ShearedLatticePeriodization.lean 12 declarations
• ShiftedBlocks.lean 30 declarations
• ShortBoxEstimate.lean 1 declarations
• ShortHorizontalLocalization.lean 2 declarations
• ShortL2Operator.lean 8 declarations
• ShortPositiveBoxes.lean 1 declarations
• ShortPositiveEnergy.lean 1 declarations
• ShortPositiveSquare.lean 1 declarations
• ShortSlopeCommutation.lean 6 declarations
• ShortSlopeL1.lean 2 declarations
• ShortSlopeLp.lean 7 declarations
• ShortSlopeLpRealization.lean 8 declarations
• ShortSlopeOperator.lean 4 declarations
• ShortTimeAverageEnergy.lean 4 declarations
• ShortTimeAverageL1.lean 2 declarations
• ShortTimeParameters.lean 2 declarations
• ShortTransformExtension.lean 1 declarations
• ShortTransformMeasurable.lean 2 declarations
• SignedPVCommutator.lean 3 declarations
• SimplexBarycenter.lean 1 declarations
• SimultaneousCount.lean 1 declarations
• SimultaneousCountPowers.lean 1 declarations
• SlicedIntegral.lean 5 declarations
• SlopeAdmissibility.lean 2 declarations
• SlopeBoxHorizontalRescale.lean 7 declarations
• SlopeBoxMask.lean 5 declarations
• SlopeMaskIntegral.lean 2 declarations
• SlopeOrthonormal.lean 6 declarations
• SlopePartition.lean 9 declarations
• SlopeTopNeighborhood.lean 3 declarations
• SmoothCarlesonEnergy.lean 4 declarations
• SmoothCarlesonEstimate.lean 1 declarations
• SmoothCarlesonSynthesis.lean 5 declarations
• SmoothPrincipalValue.lean 3 declarations
• SmoothPrincipalValueBound.lean 3 declarations
• SmoothPrincipalValueExtension.lean 1 declarations
• SmoothedCommutatorDecomposition.lean 7 declarations
• SmoothedCommutatorEnergy.lean 7 declarations
• SnappedLattice.lean 7 declarations
• SquareMaximalWeakL1.lean 8 declarations
• SquareMean.lean 1 declarations
• SquareTailLayer.lean 1 declarations
• StoppedMartingaleChain.lean 5 declarations
• StoppedMartingaleEnergy.lean 3 declarations
• StoppedScalarExpansion.lean 4 declarations
• StoppingScaleIntervals.lean 8 declarations
• StripSubdivision.lean 6 declarations
• StrongOperatorDerivative.lean 1 declarations
• SummationByParts.lean 2 declarations
• SupportedInnerIntegral.lean 1 declarations
• SynthesisPolarization.lean 3 declarations
• TailLimit.lean 1 declarations
• TerminalFlow.lean 10 declarations
• TestingWeakTwo.lean 1 declarations
• ThinTopTail.lean 1 declarations
• ThreeInputMain.lean 2 declarations
• ThresholdSynthesis.lean 5 declarations
• TileLatticeEnvelope.lean 2 declarations
• TimeEndpointComparison.lean 3 declarations
• TimeErrorEnvelope.lean 7 declarations
• TopAmplitudeBound.lean 3 declarations
• TopAreaAverage.lean 10 declarations
• TopAreaDiscard.lean 2 declarations
• TopBoxDecay.lean 2 declarations
• TopBoxPolynomial.lean 2 declarations
• TopCovariantContinuity.lean 5 declarations
• TopCovariantData.lean 2 declarations
• TopCovariantHorizontalRescale.lean 1 declarations
• TopDilatedTesting.lean 2 declarations
• TopDilationTail.lean 1 declarations
• TopDyadicDomination.lean 4 declarations
• TopEnvelopeDerivative.lean 2 declarations
• TopFamilyException.lean 4 declarations
• TopIntervalHorizontalRescale.lean 1 declarations
• TopLatticeDecay.lean 5 declarations
• TopLogAbsorption.lean 5 declarations
• TopMaskApproximation.lean 6 declarations
• TopMovingLogAbsorption.lean 2 declarations
• TopNeighborhood.lean 1 declarations
• TopPolynomialDecay.lean 1 declarations
• TopRawHorizontalRescale.lean 1 declarations
• TopShape.lean 4 declarations
• TopThreshold.lean 4 declarations
• TopWeakTwo.lean 1 declarations
• TopWeight.lean 14 declarations
• TopWeightIntegral.lean 14 declarations
• TopWeightedInterval.lean 3 declarations
• TopWeightedPair.lean 8 declarations
• TopWindowMoments.lean 1 declarations
• TotalBinError.lean 1 declarations
• TotalBinErrorScale.lean 5 declarations
• Truncation.lean 4 declarations
• TwoPointEnvelope.lean 4 declarations
• UniformPlanarRawBounds.lean 1 declarations
• UniformPolynomialMoments.lean 1 declarations
• UniformTranslatedProfileBounds.lean 12 declarations
• VariableEndpointOperator.lean 6 declarations
• VariationContinuous.lean 2 declarations
• VariationDifference.lean 4 declarations
• VariationDisjointExact.lean 7 declarations
• VariationIntervals.lean 4 declarations
• VariationMeanOscillation.lean 1 declarations
• VariationMeasurable.lean 4 declarations
• VariationPerturbation.lean 6 declarations
• VariationScalar.lean 3 declarations
• VariationSubsequence.lean 2 declarations
• VariationSum.lean 7 declarations
• VeryShortHilbertError.lean 2 declarations
• WeakTwoIntegral.lean 3 declarations
• WeightedAmplitudeMotion.lean 2 declarations
• WeightedAverage.lean 2 declarations
• WeightedCauchySchwarz.lean 1 declarations
• WeightedDilationLayer.lean 1 declarations
• WeightedExceptionalArea.lean 4 declarations
• WeightedIntegral.lean 5 declarations
• WeightedMomentIndex.lean 5 declarations
• WeightedOrder.lean 8 declarations
• WeightedReferenceVariation.lean 6 declarations
• WeightedTranslatedProfiles.lean 4 declarations
• WitnessBinCount.lean 2 declarations
• WitnessInterval.lean 5 declarations
• WitnessTransfer.lean 7 declarations