OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactProfileEstimates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The three estimates used in the basepoint argument

  1. structure OAI.PolycyclicRecognition.CompactProfileEstimates line 15

    Source documentation

    Affine means, vanishing offsets, and deterministic suffix concentration for the same profiles and ordinary sampling laws.

    structure CompactProfileEstimates
    {P G N V W L : Type*} [MeasurableSpace N] [Mul N] [NormedAddCommGroup V] [NormedSpace ℝ V]
    [ProperSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W]
    (raw : P × G → ℝ → N → C(V, W)) (μ : ℝ → ProbabilityMeasure N)
    (q : V →L[ℝ] W) (A : L → W →L[ℝ] W) (R : ℝ) (B : ℝ → Set N) : Prop where
…