production module

`AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Taylor`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Taylor.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Taylor

Imported by

AutoSamplingTheory.TechnicalLemmas.Analysis.CalculusAutoSamplingTheory.TechnicalLemmas.Registry

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Taylor.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Taylor

/-!
# Taylor and Hessian technical lemmas

Preferred Mathlib-style import path for ASTIS-owned calculus leaves:
Hessian representative handoffs, iterated derivative norm conversion,
orthonormal-basis unit directions, and quadratic-variation algebra.

The original `TechnicalLemmas.Taylor` module remains as a compatibility
surface.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace Analysis
namespace Calculus
namespace Taylor

export AutoSamplingTheory.TechnicalLemmas.Taylor (
  hessianOpNormOfSourceHessianField
  iteratedFDerivTwoOpNormOfFDerivFDerivOpNorm
  stdOrthonormalBasisUnit
  quadraticVariationNormalizationOfCoeffDefAndVarianceOne
)

end Taylor
end Calculus
end Analysis
end TechnicalLemmas
end AutoSamplingTheory