SourceWeightedTreeEnergy.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomially weighted separated synthesis on an actual source top. The product polynomial is used only as a stronger convenient weight; its reciprocal has an integral proportional to the top area.

theorem OAI.LipschitzHilbert.schwartz_colored_energy line 16
theorem OAI.LipschitzHilbert.schwartz_colored_vector_energy line 60

theorem OAI.LipschitzHilbert.polynomial_colored_packet_energy line 78

Source documentation

Polynomial multiplication preserves the separation used in the finite colored synthesis estimate.

theorem polynomial_colored_packet_energy {N : ℕ} {κ : Type*} {ι : Fin N → Type*}
    [Fintype κ] [∀ j, Fintype (ι j)] {q : ℕ}
    (c : ∀ j, ι j → EuclideanSpace ℂ κ) (f : ∀ j, ι j → κ → SchwartzMap ℝ ℂ)
    (color : Fin N → Fin q) (lo hi : Fin N → ℝ)
    (hsep : ∀ i j, i≠j → color i=color j → hi i<lo j ∨ hi j<lo i)
    (hlow : ∀ j u k ξ, |ξ|<lo j → 𝓕 (f j u k) ξ=0)
    (hhigh : ∀ j u k ξ, hi j < |ξ| → 𝓕 (f j u k) ξ=0)
    (X Z : ∀ j, ι j → ℝ) (site : ∀ j, ι j → ℤ×ℤ) (len : Fin N → ℝ)
    (a0 b0 a r W y C : ℝ) (hr : 0<r) (hW : 0<W)
    (hlen : ∀ j, 0<len j) (hlenr : ∀ j, ∀ _ : ι j, len j≤r)
    (hinj : ∀ j, Function.Injective (site j))
    (hX : ∀ j u, X j u=a0+len j*(site j u).1)
…

theorem OAI.LipschitzHilbert.integral_le_of_slice_majorant line 122
def OAI.LipschitzHilbert.treeProductPolynomial line 140
Source documentation
A convenient product polynomial on the physical top coordinates.
```
def treeProductPolynomial (a b r W t : ℝ) (z : ℝ×ℝ) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.treeProductPolynomial_pos line 143

theorem OAI.LipschitzHilbert.SourceLatticePacket.exists_weighted_physical_tree_energy line 153

Source documentation

The original source packets have polynomially weighted separated energy on every containing top. Constants precede the finite families.

theorem exists_weighted_physical_tree_energy
    (cStar cEta CEta cb Cb : ℝ) (hcEta : 0<cEta)
    (hcb : 0≤cb) (hCb : 0≤Cb) (hgap : cStar<cEta*cb) :
    ∃ C : ℝ, 0<C ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
      (t w a b r : ℝ), 0<w → 0<r →
    ∀ c : ∀ j, ι j → EuclideanSpace ℂ κ,
      (∀ j (_u : ι j), P.length j≤r) →
      (∀ j u, |P.actualX j u-a|≤r) →
      (∀ j u, |P.actualZ j u-b|≤P.width) →
      (∀ j u k ξ η, planarAngularFourier (P.physicalPacket t j u k) (ξ,η)≠0 →
        |ξ+(t+P.rowSlope j)*η|≤cStar/P.length j ∧ cEta≤w*η ∧ w*η≤CEta) →
…

Mentions: OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarAngularFourier

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_weighted_labeled_tree_energy line 336

Source documentation

Exact slot decomposition preserves the tree weight. The only label loss is the stated bound on labels per scale.

theorem exists_weighted_labeled_tree_energy
    (cStar cEta CEta cb Cb : ℝ) (hcEta : 0<cEta)
    (hcb : 0≤cb) (hCb : 0≤Cb) (hgap : cStar<cEta*cb) :
    ∃ C : ℝ, 0<C ∧ ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type)
      (Item : ∀ j, Label j → Type) [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : SourceLabeledLattice N κ Label Item) (B : ℕ),
      (∀ j, (P.labels j).card≤B) → ∀ (t w a b r : ℝ), 0<w → 0<r →
    ∀ c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ,
      (∀ j (l : P.labels j) (_u : Item j l), P.length j≤r) →
      (∀ j l u, |P.actualX j l u-a|≤r) →
      (∀ j l u, |P.actualZ j l u-b|≤P.width) →
      (∀ j l u k ξ η, planarAngularFourier (P.physicalPacket t j l u k) (ξ,η)≠0 →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarAngularFourier