SourceAngularEnvelope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The analytic amplitude of one source top has an envelope linear in its original top weight. This retains integrability and can be summed over an angular node without a factor counting its tops.

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_fourth_envelope line 18

theorem OAI.LipschitzHilbert.AngularGrid.node_amplitude_linear_envelope line 56

Source documentation

Summing the linear envelope over a node charges its actual eligible mass and introduces no cardinality factor.

theorem node_amplitude_linear_envelope {E : Type*} [NormedAddCommGroup E]
    (grid : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
    (cutoff : ℝ) (weight : ι → X → ℝ) (amplitude : ι → E)
    (level : ℕ) (cell : ℤ) (z : X) (C : ℝ)
    (hamp : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell,
      ‖amplitude i‖ ≤ C*weight i z) :
    ‖∑ i ∈ grid.cellTops tops slope precision cutoff level cell, amplitude i‖ ≤
      C*grid.mass tops slope precision cutoff weight level cell z := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.node_amplitude_fourth_envelope line 71

Source documentation

The individual four-power envelope implies the node's linear-mass bound with only the fixed upper bound for a single top weight.

theorem node_amplitude_fourth_envelope {E : Type*} [NormedAddCommGroup E]
    (grid : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
    (cutoff : ℝ) (weight : ι → X → ℝ) (amplitude : ι → E)
    (level : ℕ) (cell : ℤ) (z : X) (A C : ℝ) (hA : 0 ≤ A)
    (hw : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell, 0 ≤ weight i z)
    (hC : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell, weight i z ≤ C)
    (hamp : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell,
      ‖amplitude i‖ ≤ A*(weight i z)^4) :
    ‖∑ i ∈ grid.cellTops tops slope precision cutoff level cell, amplitude i‖ ≤
      (A*C^3)*grid.mass tops slope precision cutoff weight level cell z := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid