production module

`AutoSamplingTheory.TechnicalLemmas.Probability`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Probability.lean.

Imports

Imported by

AutoSamplingTheory.TechnicalLemmas

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialDifferentiation
import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging
import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRisk
import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge
import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential
import AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalKernel
import AutoSamplingTheory.TechnicalLemmas.Probability.EmpiricalCovariance
import AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductPairMarginal
import AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductSupport
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation
import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel
import AutoSamplingTheory.TechnicalLemmas.Probability.LawMap
import AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasure
import AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasureIntegral
import AutoSamplingTheory.TechnicalLemmas.Probability.StdGaussianMoment
import AutoSamplingTheory.TechnicalLemmas.Probability.UniformExpectationGap
import AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct

/-!
# Probability technical lemma arsenal

Parent import surface for Mathlib-ready probability lemmas used by ASTIS:
law-map rewrites, weak-test integral transport, conditional-kernel bridges,
normalization/support and finite-mass integral scaling facts, one- and
two-coordinate finite-product probability laws, probability-one support boxes,
uniform almost-sure expectation gaps, finite adaptive-kernel hybrid telescopes,
and invariance under finite kernel powers.
-/