SourceNodeMeasurable.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the original source node ratios and the finite active path product. These are the integrands used for line-to-plane gluing, independently of any selected snapshot predictors.

theorem OAI.LipschitzHilbert.measurable_sourceNodeRatio line 19
def OAI.LipschitzHilbert.sourceActiveProduct line 29
Source documentation
Inactive indices have factor one, exactly as in the source path expansion. The threshold is tested against the original forward masses.
```
def sourceActiveProduct (n beta : X → ℕ → ℝ) (M : ℝ) (count : ℕ) (x : X) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.measurable_sourceActiveProduct line 32
theorem OAI.LipschitzHilbert.sourceActiveProduct_nonneg line 42
theorem OAI.LipschitzHilbert.sourceActiveProduct_eq_stopped_product line 54
Source documentation
The measurable active product agrees exactly with the finite prefix ending at the first mass crossing. The terminal mass may be zero.
```
theorem sourceActiveProduct_eq_stopped_product (n beta : X → ℕ → ℝ)
    (M : ℝ) (count : ℕ) (x : X) (hfinal : n x count ≤ M) (hanti : Antitone (n x)) :
    sourceActiveProduct n beta M count x =
      ∏ j ∈ Finset.range (firstMassStop (n x) count M), beta x j := by
…
```
Mentions: OAI.LipschitzHilbert.sourceActiveProduct, OAI.LipschitzHilbert.firstMassStop
theorem OAI.LipschitzHilbert.sourceNodeRatio_nonneg line 76

theorem OAI.LipschitzHilbert.AngularGrid.source_packet_node_ratio_measurable line 89

Source documentation

Actual packet amplitudes and original cell masses give measurable node ratios, including at zero masses.

theorem source_packet_node_ratio_measurable {τ σ : Type*}
    (g : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
    (weight : τ → X → ℝ) (hw : ∀ t, Measurable (weight t))
    (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → τ)
    (stop : σ → ℕ) (value : X → σ → EuclideanSpace ℂ κ)
    (hv : ∀ s, Measurable (fun x => value x s)) (phase : ℕ → ℂ) (a α p : ℝ)
    (lower upper : ℕ) (parent : ℤ) :
    let cells := g.sourceBlockCells tops slope precision cutoff lower upper parent
…

Mentions: OAI.LipschitzHilbert.AngularGrid