OAI/MeasureTheory/DyadicAvoidance/AdaptiveLabels.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.AdaptiveLabels.measure_injective_constraints line 14

   Source documentation

   Distinct table addresses read independent labels, including when some addresses in the table are unused.

   theorem measure_injective_constraints
       {I : Type u_I} {K : Type u_K} {B : Type u_B} [Fintype I] [Fintype K] [MeasurableSpace B]
       (ν : Measure B) [IsProbabilityMeasure ν]
       (addr : I → K) (hinj : Function.Injective addr)
       (s : I → Set B) (hs : ∀ i, MeasurableSet (s i)) :
       (Measure.pi (fun _ : K => ν)) {ω | ∀ i, ω (addr i) ∈ s i} =
         ∏ i, ν (s i) := by
   …

2. theorem OAI.Problem310.AdaptiveLabels.measure_adaptive_constraints line 38

   Source documentation

   An address choice may depend arbitrarily on a separate selector outcome. After fixing that outcome, injectivity is the only required terminal-table fact.

   theorem measure_adaptive_constraints
       {A : Type u_A} {I : Type u_I} {K : Type u_K} {B : Type u_B} [MeasurableSpace A] [Fintype I] [Fintype K]
       [MeasurableSpace B] (μ : Measure A) (ν : Measure B)
       [IsProbabilityMeasure ν]
       (addr : A → I → K) (hinj : ∀ a, Function.Injective (addr a))
       (s : A → I → Set B) (hs : ∀ a i, MeasurableSet (s a i))
       (hmeas : MeasurableSet {z : A × (K → B) |
         ∀ i, z.2 (addr z.1 i) ∈ s z.1 i}) :
       (μ.prod (Measure.pi (fun _ : K => ν)))
         {z : A × (K → B) | ∀ i, z.2 (addr z.1 i) ∈ s z.1 i} =
         ∫⁻ a, ∏ i, ν (s a i) ∂μ := by
   …

3. theorem OAI.Problem310.AdaptiveLabels.measure_adaptive_failures line 57

   Source documentation

   The conditional failure probability of adaptively addressed Boolean tests. Only active tests impose a zero label; distinct active addresses suffice here because we assume the stronger, routing-friendly injectivity of all addresses.

   theorem measure_adaptive_failures
       {A : Type u_A} {I : Type u_I} {K : Type u_K} [MeasurableSpace A] [Fintype I] [Fintype K]
       (μ : Measure A) (ν : Measure Bool) [IsProbabilityMeasure ν]
       (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) | ∀ i, active z.1 i → z.2 (addr z.1 i) = false} =
         ∫⁻ a, (ν {false}) ^ (Finset.univ.filter (active a)).card ∂μ := by
   …

4. theorem OAI.Problem310.AdaptiveLabels.measure_adaptive_label line 87

   Source documentation

   Looking up one terminal label at a selector-dependent address preserves its marginal law. This is the pointwise mean-density identity for the routed set.

   theorem measure_adaptive_label
       {A : Type u_A} {K : Type u_K} {B : Type u_B} [MeasurableSpace A] [Fintype K]
       [MeasurableSpace B] (μ : Measure A) (ν : Measure B)
       [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
       (addr : A → K) (s : Set B) (hs : MeasurableSet s)
       (hmeas : MeasurableSet {z : A × (K → B) | z.2 (addr z.1) ∈ s}) :
       (μ.prod (Measure.pi (fun _ : K => ν)))
         {z : A × (K → B) | z.2 (addr z.1) ∈ s} = ν s := by
   …