OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedTreeMaximal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.continuous_interval_max line 16
2. theorem OAI.LipschitzHilbert.interval_max_le_variation line 31

   Also declared: OAI/Analysis/LipschitzHilbert/Geometry/SourceTransverseTreeMaximal.lean:12 (same declaration text).

3. theorem OAI.LipschitzHilbert.integral_of_nonnegative_lintegral line 37
4. theorem OAI.LipschitzHilbert.interval_max_sum_le line 48

   Also declared: OAI/Analysis/LipschitzHilbert/Geometry/SourceTransverseTreeMaximal.lean:18 (same declaration text).

5. def OAI.LipschitzHilbert.SourceLatticePacket.physicalTreePartial line 69
6. def OAI.LipschitzHilbert.SourceLatticePacket.physicalTreeVariation line 73
7. def OAI.LipschitzHilbert.SourceLatticePacket.physicalTreeMaximal line 77
8. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalTreePartial_continuous line 81
9. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalTreeVariation_continuous line 96
10. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalTreeMaximal_continuous line 100
11. theorem OAI.LipschitzHilbert.SourceLatticePacket.exists_weighted_physical_tree_variation line 106

    Source documentation

    A stronger cubic-variation estimate implies the actual interval maximum. All polynomial and Fourier scales remain those of the source.

    theorem exists_weighted_physical_tree_variation (hL : LepingleInput)
        (cStar cEta CEta cb Cb : ℝ) (hcStar : 0≤cStar) (hcEta : 0<cEta)
        (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.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarAngularFourier

12. theorem OAI.LipschitzHilbert.SourceLatticePacket.exists_weighted_physical_tree_maximal line 300

    Source documentation

    The maximum is the literal maximum of all interval sums, including empty intervals. It inherits the stronger variation energy estimate.

    theorem exists_weighted_physical_tree_maximal (hL : LepingleInput)
        (cStar cEta CEta cb Cb : ℝ) (hcStar : 0≤cStar) (hcEta : 0<cEta)
        (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.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarAngularFourier

13. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreePartial line 347
14. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeMaximal line 354
15. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreePartial_continuous line 358
16. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeMaximal_continuous line 373
17. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_weighted_labeled_tree_maximal line 380

    Source documentation

    Slots partition every partial sum, so maximal synthesis costs only one fixed label-count factor.

    theorem exists_weighted_labeled_tree_maximal (hL : LepingleInput)
        (cStar cEta CEta cb Cb : ℝ) (hcStar : 0≤cStar) (hcEta : 0<cEta)
        (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.LepingleInput, OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarAngularFourier