PacketDataAssignedPathIntegral.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The inhabited reference adapters preserve every actual coefficient and masked path amplitude from the unrestricted data.

def OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedReference line 30
theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedReference_constant line 32
theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedReference_short line 39
def OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedBand line 54
Source documentation
This is the value supplied to the supported plane theorem.
```
def assignedInhabitedBand (L A : ℝ) (z : ℝ×ℝ) (p : τ×Fin N) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedBand_original line 62
theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedAmplitude_original line 90

theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedActivePath_original line 110

Source documentation

The actual active-path integrand is precisely the one integrated by the supported inhabited-family plane theorem.

theorem assignedInhabitedActivePath_original {Kb : ℕ}
    (α p M : ℝ) (shift : Fin Kb) (top : τ) (count : ℕ) (z : ℝ×ℝ) :
    grid.sourceActivePathValue tops (fun t => (T t).slope) precision cut weight K gap
      packets assigned (fun q => stop (assigned q) q.1) original
      phase a α p M shift top count z =
    grid.sourceActivePathValue tops (fun t => (T t).slope) precision cut weight K gap
      (tops ×ˢ (Finset.univ : Finset (Fin N))) Prod.fst (fun q => stop q.1 q.2) bands
      phase a α p M shift top count z := by
…

theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedPrediction_original line 127