SourcePhysicalTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Restore the physical horizontal variable and the exact coefficient normalization after proving the normalized reference tail.

theorem OAI.LipschitzHilbert.source_physical_tail line 16

Source documentation

An exact normalized-packet identity transfers a relative tail to the original physical interval. The interval scale introduces no loss.

theorem source_physical_tail (r c u H δ small large : ℝ) (hr : 0 < r) (hc : 0 < c)
    (F Q : ℝ → ℝ) (hF : Measurable F) (heq : ∀ x, F (r*x) = c*Q x)
    (hthreshold : c*small ≤ large)
    (htail : (volume.restrict (Ico u (u+H))) {x | small ≤ |Q x|} ≤
      ENNReal.ofReal δ*ENNReal.ofReal H) :
    (volume.restrict (Ico (r*u) (r*(u+H)))) {x | large ≤ |F x|} ≤
      ENNReal.ofReal δ*ENNReal.ofReal (r*H) := by
…

theorem OAI.LipschitzHilbert.eventually_source_physical_threshold line 33
Source documentation
The exact factor in the physical mixed-packet identity is P.constant * pi^2. Restoring it only changes the fixed polynomial exponent.
```
theorem eventually_source_physical_threshold (a : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ C : ℝ, C ≤ L^a →
      (C*Real.pi^2)*L^(a+4) ≤ L^(2*a+5) := by
…
```