OAI/NumberTheory/EgyptianFractions/FiniteExposureAverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.expect_pi_partition line 9

   Source documentation

   Uniform averaging over labelled samples factors over any partition of the labels.

   theorem expect_pi_partition {ι A M : Type*} [Fintype ι] [DecidableEq ι] [Fintype A]
       [AddCommMonoid M] [Module ℚ≥0 M] (p : ι → Prop) [DecidablePred p]
       (F : (ι → A) → M) :
       (𝔼 f : ι → A, F f) =
         𝔼 a : {i // p i} → A, 𝔼 b : {i // ¬p i} → A,
           F (fun i => if h : p i then a ⟨i,h⟩ else b ⟨i,h⟩) := by
   …

   Mentions: OAI.Problem337.F

2. theorem OAI.Problem337.normalized_sum_pi_partition line 25

   Source documentation

   The same partition identity in explicit normalized-sum form.

   theorem normalized_sum_pi_partition {ι A : Type*} [Fintype ι] [DecidableEq ι] [Fintype A]
       (p : ι → Prop) [DecidablePred p] (F : (ι → A) → ℂ) :
       (∑ f : ι → A, F f) / Fintype.card (ι → A) =
         (∑ a : {i // p i} → A,
           (∑ b : {i // ¬p i} → A,
             F (fun i => if h : p i then a ⟨i,h⟩ else b ⟨i,h⟩)) /
               Fintype.card ({i // ¬p i} → A)) / Fintype.card ({i // p i} → A) := by
   …

   Mentions: OAI.Problem337.F

3. lemma OAI.Problem337.expect_finset_indicator line 35

   Source documentation

   Average over a finite probability space of an indicator is its relative cardinality.

   lemma expect_finset_indicator {Ω : Type*} [Fintype Ω] [DecidableEq Ω] (B : Finset Ω) :
       (𝔼 x : Ω, if x ∈ B then (1 : ℝ) else 0) =
         (B.card : ℝ) / Fintype.card Ω := by
   …

4. theorem OAI.Problem337.conditional_average_norm_bound line 45

   Source documentation

   Exposing some variables costs only the proportion of exceptional exposures. The inner finite type can itself be a product of independent fresh sample blocks.

   theorem conditional_average_norm_bound {Ω A : Type*} [Fintype Ω] [Fintype A]
       [Nonempty Ω] [Nonempty A] (F : Ω → A → ℂ) (B : Finset Ω) (δ : ℝ)
       (hδ : 0 ≤ δ) (hunit : ∀ ω a, ‖F ω a‖ ≤ 1)
       (hgood : ∀ ω, ω ∉ B → ‖𝔼 a : A, F ω a‖ ≤ δ) :
       ‖𝔼 ω : Ω, 𝔼 a : A, F ω a‖ ≤ (B.card : ℝ) / Fintype.card Ω + δ := by
   …

   Mentions: OAI.Problem337.F

5. theorem OAI.Problem337.expect_equiv_prod line 69

   Source documentation

   A finite reindexing into exposed and fresh coordinates gives exact Fubini averaging.

   theorem expect_equiv_prod {Ω E A M : Type*} [Fintype Ω] [Fintype E] [Fintype A]
       [AddCommMonoid M] [Module ℚ≥0 M] (e : Ω ≃ E × A) (F : Ω → M) :
       (𝔼 ω : Ω, F ω) = 𝔼 x : E, 𝔼 a : A, F (e.symm (x,a)) := by
   …

   Mentions: OAI.Problem337.F

6. theorem OAI.Problem337.exposure_average_norm_bound line 79

   Source documentation

   The conditional estimate transported back to the original labelled sample space.

   theorem exposure_average_norm_bound {Ω E A : Type*}
       [Fintype Ω] [Fintype E] [Fintype A] [Nonempty E] [Nonempty A]
       (e : Ω ≃ E × A) (F : Ω → ℂ) (B : Finset E) (δ : ℝ)
       (hδ : 0 ≤ δ) (hunit : ∀ ω, ‖F ω‖ ≤ 1)
       (hgood : ∀ x, x ∉ B → ‖𝔼 a : A, F (e.symm (x,a))‖ ≤ δ) :
       ‖𝔼 ω : Ω, F ω‖ ≤ (B.card : ℝ) / Fintype.card E + δ := by
   …

   Mentions: OAI.Problem337.F

7. theorem OAI.Problem337.conditional_average_phase_bound line 90

   Source documentation

   Multipliers fixed by the exposure and of norm at most one do not spoil cancellation.

   theorem conditional_average_phase_bound {Ω A : Type*} [Fintype Ω] [Fintype A]
       [Nonempty Ω] [Nonempty A] (F : Ω → A → ℂ) (phase : Ω → ℂ)
       (B : Finset Ω) (δ : ℝ) (hδ : 0 ≤ δ)
       (hphase : ∀ ω, ‖phase ω‖ ≤ 1) (hunit : ∀ ω a, ‖F ω a‖ ≤ 1)
       (hgood : ∀ ω, ω ∉ B → ‖𝔼 a : A, F ω a‖ ≤ δ) :
       ‖𝔼 ω : Ω, 𝔼 a : A, phase ω * F ω a‖ ≤
         (B.card : ℝ) / Fintype.card Ω + δ := by
   …

   Mentions: OAI.Problem337.F

8. theorem OAI.Problem337.expect_restrict_coordinates line 106

   Source documentation

   Uniform samples on coordinates not inspected by the function can be discarded.

   theorem expect_restrict_coordinates {ι A M : Type*}
       [Fintype ι] [DecidableEq ι] [Fintype A] [Nonempty A]
       [AddCommMonoid M] [Module ℚ≥0 M] (p : ι → Prop) [DecidablePred p]
       (F : ({i // p i} → A) → M) :
       (𝔼 f : ι → A, F (fun i => f i)) = 𝔼 a : {i // p i} → A, F a := by
   …

   Mentions: OAI.Problem337.F

9. theorem OAI.Problem337.expect_injective_coordinates line 115

   Source documentation

   Sampling any injectively selected labels gives the same uniform product law.

   theorem expect_injective_coordinates {ι κ A M : Type*}
       [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
       [Fintype A] [Nonempty A] [AddCommMonoid M] [Module ℚ≥0 M]
       (e : κ ↪ ι) (F : (κ → A) → M) :
       (𝔼 f : ι → A, F (fun k => f (e k))) = 𝔼 a : κ → A, F a := by
   …

   Mentions: OAI.Problem337.F

10. theorem OAI.Problem337.injective_coordinate_event_fraction line 134

    Source documentation

    The normalized count of a coordinate event is unaffected by unused independent labels.

    theorem injective_coordinate_event_fraction {ι κ A : Type*}
        [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
        [Fintype A] [Nonempty A] (e : κ ↪ ι) (R : (κ → A) → Prop) [DecidablePred R] :
        ((Finset.univ.filter (fun f : ι → A => R (fun k => f (e k)))).card : ℝ) /
            Fintype.card (ι → A) =
          ((Finset.univ.filter R).card : ℝ) / Fintype.card (κ → A) := by
    …