OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedCellSupremum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.packetNormSup_weighted_le line 15

   Source documentation

   A pointwise weighted comparison passes to the actual packet supremum.

   theorem packetNormSup_weighted_le {X E ι : Type*} [NormedAddCommGroup E]
       (F G : ι → X → E) (Q : Set X) (c d B : ℝ)
       (hc : 0<c) (hd : 0≤d) (hB : 0≤B)
       (hG : ∀ a x, x∈Q → ‖G a x‖≤B)
       (hFG : ∀ a x, x∈Q → c*‖F a x‖≤d*‖G a x‖) :
       c*packetNormSup F Q≤d*packetNormSup G Q := by
   …

   Mentions: OAI.LipschitzHilbert.packetNormSup

2. theorem OAI.LipschitzHilbert.finite_weighted_box_supremum_energy line 37

   Source documentation

   The polynomial power on each transverse cell is paid for by the energy of the polynomially localized packet family, uniformly in the number of cells and packets.

   theorem finite_weighted_box_supremum_energy
       (s : Finset J) (Kx Ky : SchwartzMap ℝ ℂ)
       (F : J → ι → SchwartzMap (ℝ×ℝ) (EuclideanSpace ℂ κ))
       (q : ℕ) (b W Rx Ry : ℝ) (hW : 0<W) (cx rx n : J → ℝ)
       (hrx : ∀ j∈s, 0<rx j)
       (hKx : ∀ ξ, |ξ|≤Rx → 𝓕 Kx ξ=1) (hKy : ∀ η, |η|≤Ry → 𝓕 Ky η=1)
       (hFx : ∀ j∈s, ∀ a y ξ, 𝓕 (vectorHorizontalSlice (F j a) y) ξ≠0 → |ξ|≤Rx/rx j)
       (hFy : ∀ j∈s, ∀ a x η, 𝓕 (vectorVerticalSlice (F j a) x) η≠0 → |η|≤Ry/(W/2))
       (A : J → Set (ℝ×ℝ)) (hA : ∀ j∈s, MeasurableSet (A j))
       (hAfin : ∀ j∈s, (volume.prod volume) (A j)≠∞)
       (hsub : ∀ j∈s, A j⊆coordinateBox (cx j) (b+n j*W) (rx j) (W/2))
       (hdisj : Set.Pairwise (↑s) (Disjoint on A))
   …

   Mentions: OAI.LipschitzHilbert.vectorHorizontalSlice, OAI.LipschitzHilbert.vectorVerticalSlice, OAI.LipschitzHilbert.coordinateBox