OAI/MeasureTheory/DyadicAvoidance/ExposureMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.ExposureMoments.map_restrict_eq_smul_of_fibers line 13

   Source documentation

   Joint masses of complete finite/countable patterns determine the law after restriction to an exposure event. No division by the mass of the event is needed.

   theorem map_restrict_eq_smul_of_fibers
       {A : Type u_A} {V : Type u_V} [MeasurableSpace A] [MeasurableSpace V]
       [Countable V] [MeasurableSingletonClass V]
       (μ : Measure A) (ν : Measure V) (E : Set A) (f : A → V)
       (hf : Measurable f)
       (hjoint : ∀ v, μ (E ∩ {a | f a = v}) = μ E * ν {v}) :
       Measure.map f (μ.restrict E) = μ E • ν := by
   …

2. theorem OAI.Problem310.ExposureMoments.lintegral_restrict_comp_of_fibers line 30

   Source documentation

   The exposure factorization extends from pattern events to every nonnegative function of the fresh pattern, including the active-test generating function.

   theorem lintegral_restrict_comp_of_fibers
       {A : Type u_A} {V : Type u_V} [MeasurableSpace A] [MeasurableSpace V]
       [Countable V] [MeasurableSingletonClass V]
       (μ : Measure A) (ν : Measure V) (E : Set A) (f : A → V)
       (hf : Measurable f)
       (hjoint : ∀ v, μ (E ∩ {a | f a = v}) = μ E * ν {v})
       (g : V → ENNReal) (hg : Measurable g) :
       (∫⁻ a in E, g (f a) ∂μ) = μ E * ∫⁻ v, g v ∂ν := by
   …

3. theorem OAI.Problem310.ExposureMoments.lintegral_restrict_comp_eq_of_fibers line 44

   Source documentation

   A supplied fresh-pattern moment can be used unchanged after center exposure.

   theorem lintegral_restrict_comp_eq_of_fibers
       {A : Type u_A} {V : Type u_V} [MeasurableSpace A] [MeasurableSpace V]
       [Countable V] [MeasurableSingletonClass V]
       (μ : Measure A) (ν : Measure V) (E : Set A) (f : A → V)
       (hf : Measurable f)
       (hjoint : ∀ v, μ (E ∩ {a | f a = v}) = μ E * ν {v})
       (g : V → ENNReal) (hg : Measurable g) (q : ENNReal)
       (hmoment : (∫⁻ v, g v ∂ν) = q) :
       (∫⁻ a in E, g (f a) ∂μ) = μ E * q := by
   …