OAI/Analysis/LipschitzHilbert/Trees/SourceBoxSupremum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.packetNormValues line 14
2. def OAI.LipschitzHilbert.packetNormSup line 17
3. theorem OAI.LipschitzHilbert.packetNormValues_bddAbove line 20
4. theorem OAI.LipschitzHilbert.packetNormSup_nonneg line 28
5. theorem OAI.LipschitzHilbert.packetNormSup_le line 33
6. theorem OAI.LipschitzHilbert.packetNormSup_cell_energy line 46

   Source documentation

   Integrating a common pointwise majorant controls a literal supremum on any finite-measure cell.

   theorem packetNormSup_cell_energy (μ : Measure X) (F : ι → X → E) (Q A : Set X)
       (hA : MeasurableSet A) (hAfin : μ A≠∞)
       (B C : ℝ) (hB : 0≤B) (hC : 0≤C)
       (hF : ∀ a x, x∈Q → ‖F a x‖≤B)
       (g : X → ℝ) (hg : MemLp g 2 μ) (hg0 : ∀ x, 0≤g x)
       (hpoint : ∀ᵐ z ∂μ, z∈A → ∀ a x, x∈Q → ‖F a x‖≤C*g z) :
       (packetNormSup F Q)^2*μ.real A≤C^2*∫ z in A, (g z)^2 ∂μ := by
   …

   Mentions: OAI.LipschitzHilbert.packetNormSup

7. theorem OAI.LipschitzHilbert.packetNormSup_finite_energy line 65

   Source documentation

   Disjoint cell summation does not introduce a cell-count factor.

   theorem packetNormSup_finite_energy {J : Type*} (μ : Measure X) (s : Finset J)
       (F : J → ι → X → E) (Q A : J → Set X)
       (hA : ∀ j∈s, MeasurableSet (A j)) (hAfin : ∀ j∈s, μ (A j)≠∞)
       (hdisj : Set.Pairwise (↑s) (Disjoint on A))
       (B C : ℝ) (hB : 0≤B) (hC : 0≤C)
       (hF : ∀ j∈s, ∀ a x, x∈Q j → ‖F j a x‖≤B)
       (g : X → ℝ) (hg : MemLp g 2 μ) (hg0 : ∀ x, 0≤g x)
       (hpoint : ∀ j∈s, ∀ᵐ z ∂μ, z∈A j → ∀ a x, x∈Q j → ‖F j a x‖≤C*g z) :
       (∑ j∈s, (packetNormSup (F j) (Q j))^2*μ.real (A j))≤
         C^2*∫ z, (g z)^2 ∂μ := by
   …

   Mentions: OAI.LipschitzHilbert.packetNormSup