SourceBoundedTreeSize.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded test functions have uniformly bounded coefficient size on a separated source tree. The proof uses the actual analyzing integrals, polynomially weighted synthesis and an integrable reciprocal weight.

theorem OAI.LipschitzHilbert.analyzingCoefficient_bounded_energy_le line 16

Source documentation

Weighted synthesis duality needs only a bounded test function.

theorem analyzingCoefficient_bounded_energy_le
    {X I K : Type*} [MeasurableSpace X] [Fintype I] [Fintype K]
    (μ : Measure X) (area : I → ℝ) (wave : I → K → X → ℂ)
    (g : X → EuclideanSpace ℂ K) (weight : X → ℝ) (A V M : ℝ)
    (hA : 0≤A) (hV : 0≤V) (hM : 0≤M)
    (ha : ∀ i, 0<area i) (hw : ∀ x, 0<weight x)
    (hrec : MemLp (fun x => (weight x)⁻¹) 2 μ)
    (hinv : (∫ x, ((weight x)⁻¹)^2 ∂μ)≤V)
    (hg : ∀ x, ‖g x‖≤M)
    (hint : ∀ i k, Integrable (fun x => g x k * conj (wave i k x)) μ)
    (hsyn : ∀ c, MemLp (fun x => weight x • diagonalSynthesis wave c x) 2 μ)
    (hbound : ∀ c, (∫ x, ‖weight x • diagonalSynthesis wave c x‖^2 ∂μ) ≤
…

Mentions: OAI.LipschitzHilbert.diagonalSynthesis

theorem OAI.LipschitzHilbert.treeProductPolynomial_reciprocal line 83

Source documentation

The reciprocal polynomial square is integrable with only the top area as its scale. The slope shear has Jacobian one.

theorem treeProductPolynomial_reciprocal (a b r W t : ℝ) (hr : 0<r) (hW : 0<W) :
    MemLp (fun z => (treeProductPolynomial a b r W t z)⁻¹) 2 (volume.prod volume) ∧
    (∫ z, ((treeProductPolynomial a b r W t z)⁻¹)^2 ∂volume.prod volume) ≤
      4*Real.pi^2*r*W := by
…

Mentions: OAI.LipschitzHilbert.treeProductPolynomial

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_physical_bounded_tree_size line 144

Source documentation

A bounded test has bounded size on a separated physical source tree. The constant is independent of the finite scale, packet and vector types.

theorem exists_physical_bounded_tree_size
    (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 →
    ∀ (beta : P.PacketIndex → κ → ℂ) (g : ℝ×ℝ → EuclideanSpace ℂ κ) (M : ℝ),
      0≤M → (∀ q k, ‖beta q k‖≤1) → Measurable g → (∀ z, ‖g z‖≤M) →
      (∀ 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) →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_selected_physical_bounded_tree_size line 239

Source documentation

Restriction is literal: packets outside the selected tree add no hypotheses and the original physical analyzing integrals are retained.

theorem exists_selected_physical_bounded_tree_size
    (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 →
    ∀ (beta : P.PacketIndex → κ → ℂ) (packets : Finset P.PacketIndex)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (M : ℝ),
      0≤M → (∀ q ∈ packets, ∀ k, ‖beta q k‖≤1) → Measurable g → (∀ z, ‖g z‖≤M) →
      (∀ q ∈ packets, P.length q.1≤r) →
      (∀ q ∈ packets, |P.actualX q.1 q.2.1 q.2.2-a|≤r) →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_frozen_multiplier_bounded_tree_size line 290

Source documentation

The same size bound for the original source multiplier coefficient, with the selector frozen at the tree direction.

theorem exists_frozen_multiplier_bounded_tree_size
    (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 z r : ℝ), 0<w → 0<r →
    ∀ (b : ∀ j, P.labels j → κ → ℝ → ℂ) (packets : Finset P.PacketIndex)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (M : ℝ),
      0≤M → (∀ q ∈ packets, ∀ k, ‖b q.1 q.2.1 k t‖≤1) →
      Measurable g → (∀ x, ‖g x‖≤M) →
      (∀ q ∈ packets, P.length q.1≤r) →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice