FiniteInterpolation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite bilinear interpolation with constant one

This is the finite simple-function step of §7. The analytic family is constructed explicitly, and Hadamard's theorem proves the interpolated pairing estimate from its two endpoint estimates.

def OAI.LipschitzHilbert.PhaseCombinatorics.finitePairing line 21
theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_finitePairing_le line 24
def OAI.LipschitzHilbert.PhaseCombinatorics.pairingFamily line 41
theorem OAI.LipschitzHilbert.PhaseCombinatorics.differentiable_pairingFamily line 45
theorem OAI.LipschitzHilbert.PhaseCombinatorics.pairingFamily_bddAbove line 56

theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_pairing_interpolation line 81

Source documentation

The exact normalized finite pairing estimate supplied by the coefficient and simple-test-function interpolation families.

theorem finite_pairing_interpolation (K : ι → κ → ℂ) (w : κ → ℝ)
    (hK : ∀ i j, ‖K i j‖ ≤ w j)
    {r s r₄ t : ℝ} (hr : 0 < r) (hs : 0 < s) (hr₄ : 0 < r₄)
    (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
    (hrdef : (1 - t) * (r / 1) + t * (r / r₄) = 1)
    (hsdef : (1 - t) * (s / 1) + t * (s / (4 / 3)) = 1)
    (hfour : ∀ (a : ι → ℂ) (b : κ → ℂ),
      (∑ i, ‖a i‖ ^ r₄) = 1 → (∑ j, w j * ‖b j‖ ^ (4 / 3 : ℝ)) = 1 →
      ‖finitePairing K a b‖ ≤ 1)
    (a : ι → ℂ) (b : κ → ℂ)
    (ha : (∑ i, ‖a i‖ ^ r) = 1) (hb : (∑ j, w j * ‖b j‖ ^ s) = 1) :
    ‖finitePairing K a b‖ ≤ 1 := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.finitePairing

theorem OAI.LipschitzHilbert.PhaseCombinatorics.finitePairing_div_right line 120

theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_pairing_interpolation_test line 127

Source documentation

Scaling removes the unit-norm restriction on the simple test. The coefficient sequence remains normalized.

theorem finite_pairing_interpolation_test (K : ι → κ → ℂ) (w : κ → ℝ)
    (hw : ∀ j, 0 ≤ w j) (hK : ∀ i j, ‖K i j‖ ≤ w j)
    {r s r₄ t : ℝ} (hr : 0 < r) (hs : 0 < s) (hr₄ : 0 < r₄)
    (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
    (hrdef : (1 - t) * (r / 1) + t * (r / r₄) = 1)
    (hsdef : (1 - t) * (s / 1) + t * (s / (4 / 3)) = 1)
    (hfour : ∀ (a : ι → ℂ) (b : κ → ℂ),
      (∑ i, ‖a i‖ ^ r₄) = 1 → (∑ j, w j * ‖b j‖ ^ (4 / 3 : ℝ)) = 1 →
      ‖finitePairing K a b‖ ≤ 1)
    (a : ι → ℂ) (b : κ → ℂ) (ha : (∑ i, ‖a i‖ ^ r) = 1) :
    ‖finitePairing K a b‖ ≤ (∑ j, w j * ‖b j‖ ^ s) ^ (1 / s) := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.finitePairing