OAI/MeasureTheory/DyadicAvoidance/FixedScaleProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.FixedScaleProbability.measure_exposed_adaptive_failures_eq_lintegral line 17

   Source documentation

   Exposing selector coordinates does not change the adaptive terminal-label calculation: first restrict the selector measure, then integrate out terminals.

   theorem measure_exposed_adaptive_failures_eq_lintegral
       {A : Type u_A} {I : Type u_I} {K : Type u_K} [MeasurableSpace A] [Fintype I] [Fintype K]
       (μ : Measure A) [SFinite μ] (ν : Measure Bool) [IsProbabilityMeasure ν]
       (E : Set A) (addr : A → I → K)
       (hinj : ∀ a, Function.Injective (addr a))
       (active : A → I → Prop) [∀ a i, Decidable (active a i)]
       (hmeas : MeasurableSet {z : A × (K → Bool) |
         ∀ i, active z.1 i → z.2 (addr z.1 i) = false}) :
       (μ.prod (Measure.pi (fun _ : K => ν)))
         {z : A × (K → Bool) | z.1 ∈ E ∧
           ∀ i, active z.1 i → z.2 (addr z.1 i) = false} =
         ∫⁻ a in E, (ν {false}) ^ (Finset.univ.filter (active a)).card ∂μ := by
   …

2. theorem OAI.Problem310.FixedScaleProbability.measure_exposed_adaptive_failures line 41

   Source documentation

   Fixed-scale failure on an exposure atom is its mass times the fresh-selector moment. The selected terminal addresses may depend on every selector coordinate.

   theorem measure_exposed_adaptive_failures
       {A : Type u_A} {I : Type u_I} {K : Type u_K} [MeasurableSpace A] [Fintype I] [Fintype K]
       (μ : Measure A) [SFinite μ] (ν : Measure Bool) [IsProbabilityMeasure ν]
       (E : Set A) (addr : A → I → K)
       (hinj : ∀ a, Function.Injective (addr a))
       (fresh : A → I → Bool) (hfresh : Measurable fresh)
       (σ : Measure (I → Bool))
       (hjoint : ∀ v, μ (E ∩ {a | fresh a = v}) = μ E * σ {v})
       (q : ENNReal)
       (hmoment : (∫⁻ v, (ν {false}) ^
         (Finset.univ.filter (fun i => v i = true)).card ∂σ) = q)
       (hmeas : MeasurableSet {z : A × (K → Bool) |
   …

3. theorem OAI.Problem310.FixedScaleProbability.measure_fixed_scale_on_center_atom line 68

   Source documentation

   Exact fixed-scale miss probability on a center-exposure atom. Selector lookups are fair, fresh and pairwise distinct. Terminal addresses may depend on all selectors, but their injectivity must hold for every selector outcome. This is the finite-product version of the conditional estimate.

   theorem measure_fixed_scale_on_center_atom
       {C : Type u_C} {I : Type u_I} {S : Type u_S} {T : Type u_T} [Fintype C] [Fintype I] [Fintype S] [Fintype T]
       (νs νt : Measure Bool) [IsProbabilityMeasure νs] [IsProbabilityMeasure νt]
       (hfalse : νs {false} = 1 / 2) (htrue : νs {true} = 1 / 2)
       (center : C → S) (fresh : I → S)
       (hinj : Function.Injective (Sum.elim center fresh)) (value : C → Bool)
       (addr : (S → Bool) → I → T) (haddr : ∀ a, Function.Injective (addr a))
       (p : ℝ) (hp : p ≤ 1) (hterminal : νt {false} = ENNReal.ofReal (1 - p)) :
       ((Measure.pi (fun _ : S => νs)).prod (Measure.pi (fun _ : T => νt)))
         {z : (S → Bool) × (T → Bool) |
           (∀ c, z.1 (center c) = value c) ∧
           ∀ i, z.1 (fresh i) = true → z.2 (addr z.1 i) = false} =
   …

4. theorem OAI.Problem310.FixedScaleProbability.measure_fixed_scale_eq_atom_mass line 101

   Source documentation

   The preceding identity with the actual center-atom mass as coefficient, ready for summation over center exposure values.

   theorem measure_fixed_scale_eq_atom_mass
       {C : Type u_C} {I : Type u_I} {S : Type u_S} {T : Type u_T} [Fintype C] [Fintype I] [Fintype S] [Fintype T]
       (νs νt : Measure Bool) [IsProbabilityMeasure νs] [IsProbabilityMeasure νt]
       (hfalse : νs {false} = 1 / 2) (htrue : νs {true} = 1 / 2)
       (center : C → S) (fresh : I → S)
       (hinj : Function.Injective (Sum.elim center fresh)) (value : C → Bool)
       (addr : (S → Bool) → I → T) (haddr : ∀ a, Function.Injective (addr a))
       (p : ℝ) (hp : p ≤ 1) (hterminal : νt {false} = ENNReal.ofReal (1 - p)) :
       ((Measure.pi (fun _ : S => νs)).prod (Measure.pi (fun _ : T => νt)))
         {z : (S → Bool) × (T → Bool) |
           (∀ c, z.1 (center c) = value c) ∧
           ∀ i, z.1 (fresh i) = true → z.2 (addr z.1 i) = false} =
   …