production module

`AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus`

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

Imports

Imported by

AutoSamplingTheory.TechnicalLemmas.Analysis

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LaplacianProduct
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Taylor

/-!
# Calculus technical lemma arsenal

Parent import surface for calculus leaves used by SDE/Sampling proofs.
-/