RandomSetDensity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.RandomSetDensity.selectedSet line 14
Source documentation
A selector outcome chooses the terminal address read at each point.
```
def selectedSet {A : Type u_A} {K : Type u_K} (addr : A → ℝ → K) (z : A × (K → Bool)) : Set ℝ :=
…
```

theorem OAI.Problem310.RandomSetDensity.measurableSet_selectedSet line 18

Source documentation

Finite terminal tables preserve spatial measurability of the address map.

theorem measurableSet_selectedSet
    {A : Type u_A} {K : Type u_K} [Fintype K] [MeasurableSpace K] [MeasurableSingletonClass K]
    (addr : A → ℝ → K) (haddr : ∀ a, Measurable (addr a))
    (z : A × (K → Bool)) : MeasurableSet (selectedSet addr z) := by
…

Mentions: OAI.Problem310.RandomSetDensity.selectedSet

theorem OAI.Problem310.RandomSetDensity.periodic_selectedSet line 25

Source documentation

Periodicity of terminal addresses gives periodicity of every realization.

theorem periodic_selectedSet
    {A : Type u_A} {K : Type u_K} (addr : A → ℝ → K)
    (haddr : ∀ a x, addr a (x + 1) = addr a x) (z : A × (K → Bool)) :
    ∀ x : ℝ, x + 1 ∈ selectedSet addr z ↔ x ∈ selectedSet addr z := by
…

Mentions: OAI.Problem310.RandomSetDensity.selectedSet

theorem OAI.Problem310.RandomSetDensity.pointwise_probability_selectedSet line 34

Source documentation

Independence of terminal labels from selectors gives the same membership probability at every spatial point, even with adaptively selected addresses.

theorem pointwise_probability_selectedSet
    {A : Type u_A} {K : Type u_K} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
    [Fintype K] (P : Measure A) [IsProbabilityMeasure P]
    (ν : Measure Bool) [IsProbabilityMeasure ν]
    (addr : A → ℝ → K) (x : ℝ) :
    (P.prod (Measure.pi (fun _ : K => ν))) {z | x ∈ selectedSet addr z} =
      ν {true} := by
…

Mentions: OAI.Problem310.RandomSetDensity.selectedSet

theorem OAI.Problem310.RandomSetDensity.expected_density_selectedSet line 55

Source documentation

Exact first-moment density identity for the random routed set.

theorem expected_density_selectedSet
    {A : Type u_A} {K : Type u_K} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
    [Fintype K] [MeasurableSpace K] [MeasurableSingletonClass K]
    (P : Measure A) [IsProbabilityMeasure P]
    (ν : Measure Bool) [IsProbabilityMeasure ν]
    (addr : A → ℝ → K) (haddr : ∀ a, Measurable (addr a)) :
    (∫⁻ z, volume (selectedSet addr z ∩ Set.Icc (0 : ℝ) 1)
      ∂(P.prod (Measure.pi (fun _ : K => ν)))) = ν {true} := by
…

Mentions: OAI.Problem310.RandomSetDensity.selectedSet

theorem OAI.Problem310.RandomSetDensity.bernoulli_true_mass line 71
Source documentation
The standard Boolean Bernoulli law has the expected real-parameter masses.
```
theorem bernoulli_true_mass (p : unitInterval) :
    ProbabilityTheory.bernoulliMeasure true false p {true} =
      ENNReal.ofReal (p : ℝ) := by
…
```
theorem OAI.Problem310.RandomSetDensity.bernoulli_false_mass line 78

theorem OAI.Problem310.RandomSetDensity.expected_density_bernoulli line 86

Source documentation

Bernoulli specialization with exactly the ofReal p density budget.

theorem expected_density_bernoulli
    {A : Type u_A} {K : Type u_K} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
    [Fintype K] [MeasurableSpace K] [MeasurableSingletonClass K]
    (P : Measure A) [IsProbabilityMeasure P] (p : unitInterval)
    (addr : A → ℝ → K) (haddr : ∀ a, Measurable (addr a)) :
    (∫⁻ z, volume (selectedSet addr z ∩ Set.Icc (0 : ℝ) 1)
      ∂(P.prod (Measure.pi (fun _ : K =>
        ProbabilityTheory.bernoulliMeasure true false p)))) = ENNReal.ofReal (p : ℝ) := by
…

Mentions: OAI.Problem310.RandomSetDensity.selectedSet