OAI/NumberTheory/Ostmann/Construction/SmoothMatchedPrior.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.smoothCellRoleFactor line 11
2. theorem OAI.Ostmann.smoothCellRoleFactor_mem_Icc line 15
3. theorem OAI.Ostmann.deletedSmoothCellPrior_factor line 23
4. theorem OAI.Ostmann.finite_matched_smooth_prior line 33

   Source documentation

   A matched counterpart retains its exact smooth unary factors. Only its normalizing constants and reciprocal product are extracted.

   theorem finite_matched_smooth_prior {I : Type*} [Fintype I]
       (P : Finset ℕ) (E : I → Finset ℕ) (φ : ℝ → ℝ) (G : I → ℝ)
       (e : Equiv.Perm I) (x : I → P) :
       (∏ i, deletedSmoothCellPrior P (E i) φ (G i) (x (e i))) =
         Real.exp (∑ i, smoothGiantLogNormalizer (P \ E i) φ (G i)) *
           (∏ i, (x i : ℝ))⁻¹ *
             ∏ i, smoothCellRoleFactor (E (e.symm i)) φ (G (e.symm i)) (x i) := by
   …

   Mentions: OAI.Ostmann.deletedSmoothCellPrior, OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.smoothCellRoleFactor

5. theorem OAI.Ostmann.smooth_tuple_point_bound line 51

   Source documentation

   Every original smooth tuple atom has the reciprocal product bound used in the arrangement diagonal. The priors may have different cell centers.

   theorem smooth_tuple_point_bound {I : Type*} [Fintype I]
       (P : Finset ℕ) (E : I → Finset ℕ) (φ : ℝ → ℝ)
       (hφ : ∀ x, φ x ∈ Set.Icc (0 : ℝ) 1) (G : I → ℝ) (x : I → P) :
       (∏ i, deletedSmoothCellPrior P (E i) φ (G i) (x i)) ≤
         Real.exp (∑ i, smoothGiantLogNormalizer (P \ E i) φ (G i)) *
           (∏ i, (x i : ℝ))⁻¹ := by
   …

   Mentions: OAI.Ostmann.deletedSmoothCellPrior, OAI.Ostmann.smoothGiantLogNormalizer

6. theorem OAI.Ostmann.smooth_distinct_product_mass line 70

   Source documentation

   The ordered prime-product fibre costs only a factorial, while the original smooth counterpart supplies its reciprocal total product.

   theorem smooth_distinct_product_mass (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {n : ℕ} (E : Fin n → Finset ℕ) (φ : ℝ → ℝ)
       (hφ : ∀ x, φ x ∈ Set.Icc (0 : ℝ) 1) (G : Fin n → ℝ)
       (S : Finset (Fin n → P)) (hS : ∀ x ∈ S, Function.Injective x) (M : ℕ) :
       (∑ x ∈ S.filter (fun x => (∏ i, (x i : ℕ)) = M),
         ∏ i, deletedSmoothCellPrior P (E i) φ (G i) (x i)) ≤
         (n.factorial : ℝ) *
           Real.exp (∑ i, smoothGiantLogNormalizer (P \ E i) φ (G i)) * (M : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.deletedSmoothCellPrior, OAI.Ostmann.smoothGiantLogNormalizer