OAI/NumberTheory/Ostmann/Construction/SelectedPrimeFubini.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.selectedIndexEquiv line 13
2. theorem OAI.Ostmann.selectedIndexEquiv_inl line 18
3. theorem OAI.Ostmann.selectedIndexEquiv_inr line 21
4. def OAI.Ostmann.joinBulkNonbulk line 24
5. theorem OAI.Ostmann.joinBulkNonbulk_bulk line 28
6. theorem OAI.Ostmann.joinBulkNonbulk_nonbulk line 35
7. theorem OAI.Ostmann.finite_prior_selected_fubini line 42
8. theorem OAI.Ostmann.finite_prior_selected_majorant line 77

   Source documentation

   Variable nonbulk majorants are integrated with their original weights.

   theorem finite_prior_selected_majorant {σ J A : Type*}
       [Fintype σ] [Fintype J] [Fintype A]
       (slot : J ↪ σ) (μ : σ → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
       (F : (σ → A) → ℂ) (B : ({i : σ // i ∉ Set.range slot} → A) → ℝ)
       (hF : ∀ y : {i : σ // i ∉ Set.range slot} → A,
         (∀ i : {i : σ // i ∉ Set.range slot}, μ i (y i) ≠ 0) →
         ‖∑ x : J → A, ((∏ j, μ (slot j) (x j) : ℝ) : ℂ) * F (joinBulkNonbulk slot x y)‖ ≤ B y) :
       ‖∑ x : σ → A, ((∏ i, μ i (x i) : ℝ) : ℂ) * F x‖ ≤
         ∑ y : {i : σ // i ∉ Set.range slot} → A,
           (∏ i : {i : σ // i ∉ Set.range slot}, μ i (y i)) * B y := by
   …

   Mentions: OAI.Ostmann.joinBulkNonbulk

9. theorem OAI.Ostmann.finite_prior_selected_bound line 100

   Source documentation

   Uniform bounds for the literal selected-bulk means pass to the full original law, without introducing a conditional independence assumption.

   theorem finite_prior_selected_bound {σ J A : Type*}
       [Fintype σ] [Fintype J] [Fintype A]
       (slot : J ↪ σ) (μ : σ → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
       (hmass : ∀ i, ∑ a, μ i a = 1) (F : (σ → A) → ℂ) (B : ℝ)
       (hF : ∀ y : {i : σ // i ∉ Set.range slot} → A,
         (∀ i : {i : σ // i ∉ Set.range slot}, μ i (y i) ≠ 0) →
         ‖∑ x : J → A, ((∏ j, μ (slot j) (x j) : ℝ) : ℂ) * F (joinBulkNonbulk slot x y)‖ ≤ B) :
       ‖∑ x : σ → A, ((∏ i, μ i (x i) : ℝ) : ℂ) * F x‖ ≤ B := by
   …

   Mentions: OAI.Ostmann.joinBulkNonbulk

10. theorem OAI.Ostmann.original_prime_selected_bound line 124
11. theorem OAI.Ostmann.original_prime_selected_majorant line 139
12. theorem OAI.Ostmann.joinBulkNonbulk_eq_extend line 155