SourcePhysicalCoefficient.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The reference-family analyzing coefficients are exactly the original physical packet integrals. Swapping coordinates and applying the reference slope shear preserves product Lebesgue measure, including for the totalized Bochner integral without an integrability premise.

def OAI.LipschitzHilbert.sourceReferenceToPhysical line 19
Source documentation
Reference coordinates are ordered (transverse, horizontal).
```
def sourceReferenceToPhysical (t : ℝ) : (ℝ × ℝ) ≃ᵐ (ℝ × ℝ) :=
…
```
theorem OAI.LipschitzHilbert.sourceReferenceToPhysical_apply line 22
theorem OAI.LipschitzHilbert.sourceReferenceToPhysical_measurePreserving line 25
theorem OAI.LipschitzHilbert.integral_sourceReferenceToPhysical line 30
def OAI.LipschitzHilbert.SourceLatticePacket.physicalSelectedWave line 43
def OAI.LipschitzHilbert.SourceLatticePacket.physicalCoefficient line 47
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_selectedWave_physical line 54
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_mainCoefficient_physical line 73
Source documentation
The normalized coefficient is unchanged by passing from the physical packets to their reference-line family. Both the original field and the original test function are pulled back by the same map.
```
theorem family_mainCoefficient_physical (t : ℝ) (d : Fin N → ℝ)
    (v : ℝ × ℝ → ℝ) (g : ℝ × ℝ → EuclideanSpace ℂ κ)
    (j : Fin N) (u : ι j) :
    P.family.mainCoefficient d (fun z => v (sourceReferenceToPhysical t z))
      (fun z => g (sourceReferenceToPhysical t z)) j u =
      P.physicalCoefficient t d v g j u := by
…
```
Mentions: OAI.LipschitzHilbert.sourceReferenceToPhysical