FixedResidualNormalization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed outer normalization preserves a nonzero inner residual

theorem OAI.RegularPointCoordinates.fixed_amplitude_bound line 17

Source documentation

The fixed outer-bound constant makes every normalized outer norm at most one, while retaining a definite inner norm.

theorem fixed_amplitude_bound {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H]
    (x : H) {M α : ℝ} (hM : 0 < M) (hα : 0 < α) (hx : ‖x‖ ≤ M * α) :
    ‖(M * α)⁻¹ • x‖ ≤ 1 := by
…

theorem OAI.RegularPointCoordinates.fixed_coefficient_bound line 26

Source documentation

The same normalization bounds the affine coefficients uniformly.

theorem fixed_coefficient_bound {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H]
    (b : H) (k : ℝ) {M α C : ℝ} (hM : 0 < M) (hα : 0 < α)
    (hb : ‖b‖ + |k| ≤ C * α) :
    ‖(M * α)⁻¹ • b‖ + |(M * α)⁻¹ * k| ≤ C / M := by
…

theorem OAI.RegularPointCoordinates.fixed_residual_moment line 41
Source documentation
The inner diagonal moment is exactly M⁻², independent of the small residual norm. This supplies the nonzero norm in the compactness limit.
```
theorem fixed_residual_moment {n : ℕ} (s : Set X) (hfin : μ s ≠ ∞)
    (u : Fin n → SobolevSpace μ hQ) (w : SobolevSpace μ hQ)
    {M : ℝ} (hM : 0 < M)
    (hpos : 0 < ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s w)‖) :
    let α := ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s w)‖
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.amplitude_euler_identity line 61

Source documentation

Amplitude normalization preserves the exact rescaled Euler identity.

theorem amplitude_euler_identity {n : ℕ} (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (f w e : SobolevSpace μ hQ) (u : Fin n → SobolevSpace μ hQ)
    (b : Fin n → ℝ) (k a t : ℝ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hid : t • localRadialDerivative μ hQ Ω f hf w =
      SobolevSpace.restrictLp μ hQ Ω w + (∑ j, b j • SobolevSpace.restrictLp μ hQ Ω (u j)) +
      k • restrictedOne μ Ω hfin + SobolevSpace.restrictLp μ hQ Ω e) :
    t • localRadialDerivative μ hQ Ω f hf (a • w) =
      SobolevSpace.restrictLp μ hQ Ω (a • w) +
      (∑ j, (a * b j) • SobolevSpace.restrictLp μ hQ Ω (u j)) +
      (a * k) • restrictedOne μ Ω hfin + SobolevSpace.restrictLp μ hQ Ω (a • e) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne