OAI/NumberTheory/TwoPoint/Bounds/CenteredWordExpansion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.singletonSlots line 15
2. def OAI.TwoPointCorrelations.nonsingletonSlots line 18
3. lemma OAI.TwoPointCorrelations.singleton_occurrence_exists line 21
4. def OAI.TwoPointCorrelations.singletonRepresentative line 28
5. lemma OAI.TwoPointCorrelations.singletonRepresentative_label line 31
6. lemma OAI.TwoPointCorrelations.singleton_occurrence_unique line 35
7. def OAI.TwoPointCorrelations.singletonTarget line 44
8. lemma OAI.TwoPointCorrelations.singletonTarget_at line 48
9. lemma OAI.TwoPointCorrelations.singletonSlots_product line 54
10. lemma OAI.TwoPointCorrelations.centered_singleton_product line 71
11. lemma OAI.TwoPointCorrelations.centered_word_split line 84
12. lemma OAI.TwoPointCorrelations.centered_word_designation_expansion line 108

    Source documentation

    Every singleton remains centered while only nonsingleton occurrences are expanded. This is an identity of signed word contributions.

    lemma centered_word_designation_expansion [DecidableEq A]
        (label : τ → ι) (target : τ → A) (base x : ι → A) (θ : ι → ℝ)
        (R : ℝ) (G : (ι → A) → ℝ) :
        R * (∏ t, ((if x (label t) = target t then (1 : ℝ) else 0) - θ (label t))) * G x =
          ∑ U ∈ (nonsingletonSlots label).powerset,
            (R * ((-1 : ℝ) ^ U.card * ∏ t ∈ U, θ (label t))) *
              ((∏ t ∈ nonsingletonSlots label \ U,
                if x (label t) = target t then (1 : ℝ) else 0) *
                ((∏ i ∈ singletonLabels label,
                  ((if x i = singletonTarget label target base i then (1 : ℝ) else 0) - θ i)) * G x)) := by
    …

    Mentions: OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.singletonLabels, OAI.TwoPointCorrelations.singletonTarget

13. theorem OAI.TwoPointCorrelations.centered_word_expectation line 127

    Source documentation

    Averaging precedes the triangle inequality; no absolute value is introduced while expanding the signed nonsingleton terms.

    theorem centered_word_expectation [Fintype A] [DecidableEq A]
        (μ : FiniteLaw (ι → A)) (label : τ → ι) (target : τ → A)
        (base : ι → A) (θ : ι → ℝ) (R : ℝ) (G : (ι → A) → ℝ) :
        μ.average (fun x => R *
          (∏ t, ((if x (label t) = target t then (1 : ℝ) else 0) - θ (label t))) * G x) =
          ∑ U ∈ (nonsingletonSlots label).powerset, μ.average (fun x =>
            (R * ((-1 : ℝ) ^ U.card * ∏ t ∈ U, θ (label t))) *
              ((∏ t ∈ nonsingletonSlots label \ U,
                if x (label t) = target t then (1 : ℝ) else 0) *
                ((∏ i ∈ singletonLabels label,
                  ((if x i = singletonTarget label target base i then (1 : ℝ) else 0) - θ i)) * G x))) := by
    …

    Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.singletonLabels, OAI.TwoPointCorrelations.singletonTarget

14. lemma OAI.TwoPointCorrelations.singleton_disjoint_designated line 142