SourceWeightedTreeMajorant.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual polynomially weighted tree maximum is a bounded measurable majorant. Its L2 energy is inherited from the stronger product weight, without adding a maximal-function premise.

def OAI.LipschitzHilbert.SourceLabeledLattice.transverseTreeMajorant line 17
theorem OAI.LipschitzHilbert.SourceLabeledLattice.transverseTreeMajorant_nonneg line 21
theorem OAI.LipschitzHilbert.SourceLabeledLattice.transverseTreeMajorant_continuous line 27
theorem OAI.LipschitzHilbert.SourceLabeledLattice.transverseTreeMajorant_bounded line 37
Source documentation
Boundedness is obtained from the finitely many actual weighted Schwartz partial sums; the bound is needed only for representatives.
```
theorem transverseTreeMajorant_bounded (b : ℝ) (q : ℕ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ) :
    ∃ B : ℝ, 0≤B ∧ ∀ z, ‖P.transverseTreeMajorant b q c z‖≤B := by
…
```

theorem OAI.LipschitzHilbert.SourceLabeledLattice.transverseTreeMajorant_energy line 74

Source documentation

The stronger product-weight estimate supplies the exact L2 majorant needed by the compiled cell-energy theorem.

theorem transverseTreeMajorant_energy (a b r : ℝ) (q : ℕ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (E0 : ℝ)
    (hI : Integrable (fun z : ℝ×ℝ =>
      (polynomialWeight a (2*r) q z.1*polynomialWeight b (2*P.width) q z.2)^2*
        P.physicalTreeMaximal 0 c z^2) (volume.prod volume))
    (hE : (∫ z : ℝ×ℝ,
      (polynomialWeight a (2*r) q z.1*polynomialWeight b (2*P.width) q z.2)^2*
        P.physicalTreeMaximal 0 c z^2 ∂volume.prod volume)≤E0) :
    MemLp (P.transverseTreeMajorant b q c) 2 (volume.prod volume) ∧
      (∫ z, (P.transverseTreeMajorant b q c z)^2 ∂volume.prod volume)≤E0 := by
…

Mentions: OAI.LipschitzHilbert.polynomialWeight