OAI/Analysis/LipschitzHilbert/Trees/SourcePathIntegrand.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The original finite hierarchy path integrand, expressed only through packet amplitudes, top weights and the stopping threshold. Its spatial measurability does not involve the auxiliary snapshot choices.

  1. def OAI.LipschitzHilbert.AngularGrid.sourceBlockNodeRatio line 17
  2. def OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathRatio line 30
  3. def OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue line 39
  4. theorem OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue_measurable line 48
  5. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlockNodeRatio_nonneg line 64
  6. theorem OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue_nonneg line 79
  7. theorem OAI.LipschitzHilbert.AngularGrid.source_path_integrand_measurable line 94

    Source documentation

    The actual source path factor, restricted to an arbitrary measurable good set and multiplied by its distinguished top weight, is measurable.

    theorem source_path_integrand_measurable {Kb : ℕ} (g : AngularGrid) (tops : Finset τ)
    (T : τ → SlopeBox) (w cutoff Kw D : ℝ) (hKw : 0 < Kw)
    (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → τ)
    (stop : σ → ℕ) (value : (ℝ × ℝ) → σ → EuclideanSpace ℂ κ)
    (hv : ∀ s, Measurable (fun x => value x s))
    (phase : ℕ → ℂ) (a α p M : ℝ) (tag : Fin Kb) (top : τ) (count : ℕ)
    (good : Set (ℝ × ℝ)) (hgood : MeasurableSet good) :
    Measurable (good.indicator (fun x => (T top).weight Kw D x *
      g.sourceActivePathValue tops (fun t => (T t).slope) (fun t => w/(T t).length) cutoff
        (fun t x => (T t).weight Kw D x) K gap packets assigned stop value
        phase a α p M tag top count x)) := by
…

    Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox