CenterExposure.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.CenterExposure.injective_sum_addresses line 16

Source documentation

Center and fresh addresses together are injective if each family is injective and their coordinate ranges are disjoint.

theorem injective_sum_addresses {C : Type u_C} {I : Type u_I} {K : Type u_K}
    (center : C → K) (fresh : I → K)
    (hc : Function.Injective center) (hf : Function.Injective fresh)
    (hdisj : ∀ c i, center c ≠ fresh i) :
    Function.Injective (Sum.elim center fresh) := by
…

theorem OAI.Problem310.CenterExposure.measure_center_and_fresh line 35

Source documentation

Center constraints do not alter the product law of distinct fresh coordinates. This unnormalized identity avoids all conditional-expectation bookkeeping and applies to arbitrary coordinate label spaces.

theorem measure_center_and_fresh
    {C : Type u_C} {I : Type u_I} {K : Type u_K} {B : Type u_B} [Fintype C] [Fintype I] [Fintype K]
    [MeasurableSpace B] (ν : Measure B) [IsProbabilityMeasure ν]
    (center : C → K) (fresh : I → K)
    (hinj : Function.Injective (Sum.elim center fresh))
    (s : C → Set B) (t : I → Set B)
    (hs : ∀ c, MeasurableSet (s c)) (ht : ∀ i, MeasurableSet (t i)) :
    (Measure.pi (fun _ : K => ν))
      {ω | (∀ c, ω (center c) ∈ s c) ∧ (∀ i, ω (fresh i) ∈ t i)} =
      (∏ c, ν (s c)) * ∏ i, ν (t i) := by
…

theorem OAI.Problem310.CenterExposure.measure_center_atom_and_fresh line 55

Source documentation

Specialization to an atom specifying all exposed center entries.

theorem measure_center_atom_and_fresh
    {C : Type u_C} {I : Type u_I} {K : Type u_K} {B : Type u_B} [Fintype C] [Fintype I] [Fintype K]
    [MeasurableSpace B] [MeasurableSingletonClass B]
    (ν : Measure B) [IsProbabilityMeasure ν]
    (center : C → K) (fresh : I → K)
    (hinj : Function.Injective (Sum.elim center fresh))
    (value : C → B) (t : I → Set B)
    (ht : ∀ i, MeasurableSet (t i)) :
    (Measure.pi (fun _ : K => ν))
      {ω | (∀ c, ω (center c) = value c) ∧ (∀ i, ω (fresh i) ∈ t i)} =
      (∏ c, ν {value c}) * ∏ i, ν (t i) := by
…

theorem OAI.Problem310.CenterExposure.map_fresh_restrict_center_atom line 73

Source documentation

The whole fresh coordinate vector has its original product law after restricting to a center atom, multiplied only by the atom's mass. This form permits arbitrary fresh-vector events and moments, not just cylinders.

theorem map_fresh_restrict_center_atom
    {C : Type u_C} {I : Type u_I} {K : Type u_K} {B : Type u_B} [Fintype C] [Fintype I] [Fintype K] [Countable B]
    [MeasurableSpace B] [MeasurableSingletonClass B]
    (ν : Measure B) [IsProbabilityMeasure ν]
    (center : C → K) (fresh : I → K)
    (hinj : Function.Injective (Sum.elim center fresh)) (value : C → B) :
    Measure.map (fun ω : K → B => fun i => ω (fresh i))
      ((Measure.pi (fun _ : K => ν)).restrict
        {ω | ∀ c, ω (center c) = value c}) =
      (∏ c, ν {value c}) • Measure.pi (fun _ : I => ν) := by
…

theorem OAI.Problem310.CenterExposure.lintegral_fresh_restrict_center_atom line 104

Source documentation

Any nonnegative measurable function of the fresh vector has the same moment on a center atom, up to multiplication by the atom mass.

theorem lintegral_fresh_restrict_center_atom
    {C : Type u_C} {I : Type u_I} {K : Type u_K} {B : Type u_B} [Fintype C] [Fintype I] [Fintype K] [Countable B]
    [MeasurableSpace B] [MeasurableSingletonClass B]
    (ν : Measure B) [IsProbabilityMeasure ν]
    (center : C → K) (fresh : I → K)
    (hinj : Function.Injective (Sum.elim center fresh)) (value : C → B)
    (F : (I → B) → ℝ≥0∞) (hF : Measurable F) :
    (∫⁻ ω, F (fun i => ω (fresh i)) ∂
      ((Measure.pi (fun _ : K => ν)).restrict
        {ω | ∀ c, ω (center c) = value c})) =
      (∏ c, ν {value c}) * ∫⁻ v, F v ∂Measure.pi (fun _ : I => ν) := by
…