SourceAmplitudeMotion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact source analytic family inherits motion from its endpoint weights and original interval packet sums. Different endpoint coefficients allow the common top mask to be evaluated at each spatial point.

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_single_top_motion line 19

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_node_motion line 63

Source documentation

Summing the actual single-top motion bounds charges the snapshot mass of the node, with no loss from the number of eligible tops.

theorem sourcePacketAmplitude_node_motion {σ E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E]
    (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
    (cutoff : ℝ) (weight : ι → X → ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (K : ℕ) (gap : ℕ → ℝ) (bands : Finset σ) (stop : ι → σ → ℕ)
    (value0 value1 : ι → σ → E)
    (he : ∀ t ∈ tops, ∀ j ∈ bands, g.eligible cutoff (precision t) (stop t j))
    (phase : ℕ → ℂ) (a : ℝ) (z0 z1 : X) (level : ℕ) (cell : ℤ)
    (U : E →ₗᵢ[ℂ] E) (A C : ℝ) (hA : 0 ≤ A)
    (hw : ∀ t ∈ g.cellTops tops slope precision cutoff level cell, 0 ≤ weight t z0)
    (hC : ∀ t ∈ g.cellTops tops slope precision cutoff level cell, weight t z0 ≤ C)
    (hmotion : ∀ t ∈ g.cellTops tops slope precision cutoff level cell,
…

Mentions: OAI.LipschitzHilbert.AngularGrid