OAI/Analysis/LipschitzHilbert/Packets/PacketDataTreeSize.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.PacketLatticeData.reference_separated_energy_eq_sizeTest line 16
2. theorem OAI.LipschitzHilbert.PacketLatticeData.reference_selected_size_bound line 31
3. def OAI.LipschitzHilbert.PacketLatticeData.referenceTreeTop line 46
4. theorem OAI.LipschitzHilbert.PacketLatticeData.reference_piece_size_bound line 57

   Source documentation

   Global size control supplies precisely the separated energy bound needed on each centered spatial piece.

   theorem reference_piece_size_bound
       (Q R : Finset P.PacketIndex) (hQR : Q⊆R) (t a b w cb tau sigma : ℝ)
       (cell : ∀ j, P.labels j → ℤ) (grid : ℤ)
       (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
       (htime : P.topLength≤tau)
       (hX : ∀ q∈Q, |P.actualX q.1 q.2.1 q.2.2-a|≤P.topLength/2)
       (hY : ∀ q∈Q, |P.actualZ q.1 q.2.1 q.2.2-t*P.actualX q.1 q.2.1 q.2.2-b|≤P.width/2)
       (hangle : ∀ q∈Q, t∈scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1))
       (hsize : ∀ U : SlopeBox, U.width=P.width → U.length≤tau →
         P.unsignedSizeTestEnergy w cb cell grid c R U≤sigma^2*U.area) :
       (∑ q∈Q, if cb*w/P.length q.1≤|P.rowSlope q.1 q.2.1-t| then
         ‖c q.1 q.2.1 q.2.2‖^2*P.length q.1*P.width else 0)≤sigma^2*(P.topLength*P.width) := by
   …

   Mentions: OAI.LipschitzHilbert.scaledAngularCell, OAI.LipschitzHilbert.SlopeBox