OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedMaskSums.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SlopeBox.mask_zero line 14
2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue_eq_cross_at line 28
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue_zero line 41
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCrossPacketValue_continuous line 49
5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedCrossInterval_eq_rawInterval line 81

   Source documentation

   Removing the neutral mask from the already proved exact interval identity gives the unmasked original adjoint sum, without division by a mask.

   theorem assignedCrossInterval_eq_rawInterval (z : ℝ×ℝ) (top : τ)
       (hcondition : ∀ q ∈ packets, assigned q = top →
         P.referenceCondition t (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),
         P.physicalCrossPacketValue alt hAlt t b v f 0 z q) =
         ((Q top).withProfile (alts top) (halt top)).rawInterval
           (fun j l u => P.physicalMultiplierCoefficient t b v f j (orig top 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

6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedCrossSum_eq_rawInterval line 94
7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_assignedPhysicalMaskedValue line 112

   Source documentation

   The masked finite sum is exactly the sum of the same original assigned top sums multiplied by their masks.

   theorem sum_assignedPhysicalMaskedValue (tops : Finset τ)
       (hassigned : ∀ q ∈ packets, assigned q ∈ tops) (L A : ℝ) (z : ℝ×ℝ) :
       (∑ q ∈ packets, P.physicalMaskedValue alt hAlt t b v f
         (fun j l u => T (assigned ⟨j,⟨l,u⟩⟩)) L A z q) =
       ∑ top ∈ tops, (T top).mask L A z •
         ∑ q ∈ packets.filter (fun q => assigned q = top),
           P.physicalCrossPacketValue alt hAlt t b v f 0 z q := by
   …