SourceAssignedPathIntegral.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact adapters for applying the supported plane theorem to the inhabited assigned reference families. The original packet values, coefficient integrals and path predictions are preserved.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_topGeometry line 20
Source documentation
No geometric condition is lost when empty label fibers are removed.
```
theorem inhabitedFamily_topGeometry (P : SourceLabeledLattice N κ Label Item)
    (T : SlopeBox) (K : ℝ) (D : ℕ) (h : SourceLabeledTopGeometry P T K D) :
    SourceLabeledTopGeometry P.inhabitedFamily T K D := by
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledTopGeometry

theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_maskedRawBand line 30

Source documentation

Original coefficient masks and all three raw jets are unchanged.

theorem inhabitedFamily_maskedRawBand (P : SourceLabeledLattice N κ Label Item)
    (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
    (t : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (mask : ℝ) (jet : Fin 3)
    (j : Fin N) (x y : ℝ) :
    (P.inhabitedFamily.withProfile (P.inhabitedAlternate alt)
      (P.inhabitedAlternate_bound alt hAlt)).rawBand
      (fun j l u => mask • P.inhabitedFamily.physicalMultiplierCoefficient t
        (fun j l => b j (P.inhabitedOriginalLabel j l)) v f j l u) jet j x y =
    (P.withProfile alt hAlt).rawBand
      (fun j l u => mask • P.physicalMultiplierCoefficient t b v f j l u) jet j x y := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SourceLabeledLattice.rawBand

theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_rawInterval_original line 45
def OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedReference line 75
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedReference_constant line 77
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedReference_short line 84
def OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedBand line 99
Source documentation
This is the value supplied to the supported plane theorem.
```
def assignedInhabitedBand (L A : ℝ) (z : ℝ×ℝ) (p : τ×Fin N) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedBand_original line 107
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedAmplitude_original line 135

theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedActivePath_original line 155

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.SourceLabeledLattice.assignedInhabitedPrediction_original line 172