OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedBoundaryPrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalBands_interval_sum line 38

   Source documentation

   Regrouping the original packets by length preserves the exact assigned top subset.

   theorem assignedPhysicalBands_interval_sum (lower upper : ℕ) :
       (∑ j ∈ Finset.univ.filter (fun j : Fin N => lower ≤ j.val ∧ j.val < upper),
         P.assignedPhysicalBands alt hAlt oldSlope b v f
           (fun j l u => T (assigned ⟨j,⟨l,u⟩⟩)) L A packets assigned z (top,j)) =
         ∑ q ∈ packets.filter (fun q => assigned q = top ∧ lower ≤ q.1.val ∧ q.1.val < upper),
           original q := by
   …

2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalInterval_eq_maskedRawInterval line 68

   Source documentation

   Exact original masked interval, expressed by the raw assigned reference interval whose norm is bounded on the concentration good set.

   theorem assignedPhysicalInterval_eq_maskedRawInterval
       (hcondition : ∀ q ∈ packets, assigned q = top →
         P.referenceCondition oldSlope (T top).slope (R top) cone w q.1 q.2.1)
       (lower upper : ℕ) (hlu : lower ≤ upper) :
       (∑ q ∈ packets.filter (fun q => assigned q = top ∧ lower ≤ q.1.val ∧ q.1.val < upper),
         original q) =
         (T top).mask L A z • ((Q).withProfile alts halt).rawInterval
           (fun j l u => P.physicalMultiplierCoefficient oldSlope b v f j (orig j l) u.val)
           0 lower upper z.1 (z.2-(T top).slope*z.1) := by
   …

   Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.withProfile, OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval

3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalInterval_norm_le line 105
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalStoppingPrefix_norm_le line 122
5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalSourcePrefix_norm_le line 145