OAI/NumberTheory/Ostmann/Tree/SampleEqualityPatterns.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact decomposition of finite samples by equality pattern

  1. abbrev OAI.Ostmann.SampleEqualityPattern line 15

    Source documentation

    A pattern records exactly which sampled positions coincide. Its class values are distinct; independence is imposed only on their dominating product prior.

    abbrev SampleEqualityPattern (I A : Type*) :=
…
  2. def OAI.Ostmann.SampleEqualityPattern.evaluate line 18
  3. theorem OAI.Ostmann.SampleEqualityPattern.kernel_evaluate line 21
  4. def OAI.Ostmann.sampleEqualityPatternEquiv line 28

    Source documentation

    Every sample has a unique equality pattern and a unique injective assignment of values to its classes.

    noncomputable def sampleEqualityPatternEquiv (I A : Type*) :
    SampleEqualityPattern I A ≃ (I → A) :=
…

    Mentions: OAI.Ostmann.SampleEqualityPattern

  5. def OAI.Ostmann.sampleSetoidFintype line 42
  6. theorem OAI.Ostmann.sum_sample_equality_patterns line 49

    Source documentation

    This equality is a decomposition, so no number-of-samples factor is lost.

    theorem sum_sample_equality_patterns {I A : Type*} [Fintype I] [Fintype A]
    {M : Type*} [AddCommMonoid M] (f : (I → A) → M) :
    letI := sampleSetoidFintype I
…

    Mentions: OAI.Ostmann.sampleSetoidFintype