Mathlib.Analysis.RealInterpolation
For a pair of Banach spaces continuously embedded in a common vector space, the quadratic K-functional K(t, v)² is the infimum of ‖v₀‖₀² + t²·‖v₁‖₁² over decompositions v = v₀ + v₁, and the interpolation norm of exponent
Basic 7 core · 0 supporting Extended endpoint norms encode membership by the value infinity. ★ wNorm_sq
Normalized quadratic real interpolation
Extended endpoint norms encode membership by the value infinity. This module defines the squared quadratic K-functional and its normalized real interpolation energy, with exactly the normalization in Chandler-Wilde, Hewett, Moiola (2015), (8)--(9). Weighted norms are defined on measurable functions modulo null sets. No endpoint space, interpolation conclusion, or paper-specific statement is assumed here.
def kFunctionalSq reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Endpoint norms, a positive scale, and an ambient vector determine the squared quadratic K-functional: the infimum, over all ways of writing the vector as a sum of two pieces, of the squared first norm of the first piece plus t² times the squared second norm of the second piece. The definition also makes sense at arbitrary real scales.
Definition (Lean source)
parameters
def
kFunctionalSq n0 n1 t v :
ℝ≥0∞
given by
⨅ (v0 : V) (v1 : V) (_ : v = v0 + v1), n0 v0 ^ 2 + ofReal (t ^ 2) * n1 v1 ^ 2
def normalizationSq reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
An interpolation exponent determines the squared quadratic normalization constant, equal to twice the sine of π times the exponent divided by π.
def kNormSq reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Endpoint norms, an exponent, and a vector determine the normalized squared quadratic real interpolation norm. Integration uses Lebesgue measure on the positive real scales.
Definition (Lean source)
parameters
def
kNormSq n0 n1 θ v :
ℝ≥0∞
given by
def embeddedNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
A continuous linear embedding and an ambient vector determine the endpoint norm extended by infinity outside the embedding's range. Injectivity is imposed by theorems that identify this value with an endpoint norm.
Definition (Lean source)
parameters
E V :
i :
E →L[ℝ] V
v :
V
def
embeddedNorm i v :
ℝ≥0∞
given by
⨅ (e : E) (_ : i e = v), ofReal ‖e‖
def wNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
A weight, a measure, and a measurable complex function modulo null sets determine its weighted L² norm, allowing infinity.
Definition (Lean source)
def harmonicWeight reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Two endpoint weights and a scale determine the harmonic weight a·(t²·b)/(a + t²·b). Only positive finite weights are used in identities.
theorem wNorm_sq reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
The square of the weighted L² norm is the weighted squared energy of the function for the weight and measure, including infinite energies.
Formal statement
hypotheses
conclusion
wNorm w μ f ^ 2 = ∫⁻ x, w x * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ
Proof (Lean source)
theorem wNorm_sq {S : Type*} [MeasurableSpace S] (w : S → ℝ≥0∞)
(μ : Measure S) (f : S →ₘ[μ] ℂ) :
wNorm w μ f ^ 2 = ∫⁻ x, w x * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ := by
unfold wNorm
simpa using ENNReal.rpow_inv_natCast_pow (n := 2) (by decide)
(∫⁻ x, w x * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ)
Endpoint 1 core · 4 supporting These order-theoretic lemmas identify the extended ambient norm and translate ambient decompositions to endpoint decompositions. ★ kFunctionalSq_embedded
Embedded endpoint norms and decomposition infima
These order-theoretic lemmas identify the extended ambient norm and translate ambient decompositions to endpoint decompositions. Positivity of the scale is essential when eliminating an infinite endpoint cost. The final lemma is the rescaled K-functional estimate, before integrating in the scale.
theorem kFunctionalSq_embedded reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Injective endpoint embeddings identify the ambient quadratic K-functional with the endpoint decomposition infimum, at a positive scale and an ambient vector.
Formal statement
hypotheses
E0 E1 V :
i0 :
E0 →L[ℝ] V
i1 :
E1 →L[ℝ] V
hi0 :
Injective i0
hi1 :
Injective i1
t :
ℝ
ht :
0 < t
v :
V
conclusion
= ⨅ (e0 : E0) (e1 : E1) (_ : v = i0 e0 + i1 e1), ofReal ‖e0‖ ^ 2
Proof (Lean source)
theorem kFunctionalSq_embedded {E0 E1 V : Type*}
[NormedAddCommGroup E0] [NormedSpace ℝ E0]
[NormedAddCommGroup E1] [NormedSpace ℝ E1]
[NormedAddCommGroup V] [NormedSpace ℝ V]
(i0 : E0 →L[ℝ] V) (i1 : E1 →L[ℝ] V)
(hi0 : Injective i0) (hi1 : Injective i1)
(t : ℝ) (ht : 0 < t) (v : V) :
kFunctionalSq (embeddedNorm i0) (embeddedNorm i1) t v =
⨅ (e0 : E0) (e1 : E1) (_ : v = i0 e0 + i1 e1),
ofReal ‖e0‖ ^ 2 + ofReal (t ^ 2) * ofReal ‖e1‖ ^ 2 := by
classical
unfold kFunctionalSq
apply le_antisymm
· refine le_iInf fun e0 => le_iInf fun e1 => le_iInf fun h => ?_
refine (iInf_le_of_le (i0 e0) (iInf_le_of_le (i1 e1)
(iInf_le_of_le h le_rfl))).trans ?_
rw [embeddedNorm_apply i0 hi0, embeddedNorm_apply i1 hi1]
· refine le_iInf fun v0 => le_iInf fun v1 => le_iInf fun h => ?_
by_cases h0 : v0 ∈ range i0
· obtain ⟨e0, rfl⟩ := h0
by_cases h1 : v1 ∈ range i1
· obtain ⟨e1, rfl⟩ := h1
rw [embeddedNorm_apply i0 hi0, embeddedNorm_apply i1 hi1]
exact iInf_le_of_le e0 (iInf_le_of_le e1 (iInf_le_of_le h le_rfl))
· rw [embeddedNorm_eq_top i1 v1 h1]
have ht' : ofReal (t ^ 2) ≠ 0 :=
ne_of_gt (ENNReal.ofReal_pos.mpr (sq_pos_of_pos ht))
simp [ENNReal.mul_top, ht']
· rw [embeddedNorm_eq_top i0 v0 h0]
simp
4 supporting declarations (lemmas, instances)
-
embeddedNorm_applytheorem — An injective embedding gives the original endpoint norm at an embedded vector.Proof (Lean source)
theorem embeddedNorm_apply {E V : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : E →L[ℝ] V) (hi : Injective i) (e : E) : embeddedNorm i (i e) = ofReal ‖e‖ := by unfold embeddedNorm apply le_antisymm · exact iInf_le_of_le e (iInf_le_of_le rfl le_rfl) · refine le_iInf fun e' => le_iInf fun h => ?_ rw [hi h] -
embeddedNorm_eq_toptheorem — A vector outside the range of an embedding has infinite extended endpoint norm.Proof (Lean source)
theorem embeddedNorm_eq_top {E V : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : E →L[ℝ] V) (v : V) (hv : v ∉ range i) : embeddedNorm i v = ⊤ := by unfold embeddedNorm refine iInf_eq_top.mpr fun e => iInf_eq_top.mpr fun h => ?_ exact (hv ⟨e, h⟩).elim -
embeddedNorm_lt_top_ifftheorem — An injective embedding gives a finite extended norm exactly on its range, at any ambient vector.Proof (Lean source)
theorem embeddedNorm_lt_top_iff {E V : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : E →L[ℝ] V) (hi : Injective i) (v : V) : embeddedNorm i v < ⊤ ↔ ∃ e, i e = v := by constructor · intro h by_contra hn have hv : v ∉ range i := hn rw [embeddedNorm_eq_top i v hv] at h exact (lt_irrefl _ h) · rintro ⟨e, rfl⟩ rw [embeddedNorm_apply i hi e] exact ENNReal.ofReal_lt_top -
kFunctionalSq_map_letheorem — An additive operator with positive finite endpoint bounds satisfies the rescaled squared K-functional estimate, for endpoint gauges, a positive scale, and a vector.hypothesesV W :n0 n1 :V → ℝ≥0∞m0 m1 :W → ℝ≥0∞D :V →+ WA0 A1 :ℝ≥0∞hA0 :0 < A0 ∧ A0 < ⊤hA1 :0 < A1 ∧ A1 < ⊤h0 :∀ v, m0 (D v) ≤ A0 * n0 vh1 :∀ v, m1 (D v) ≤ A1 * n1 vt :ℝht :0 < tv :VconclusionkFunctionalSq m0 m1 t (D v) ≤ A0 ^ 2 * kFunctionalSq n0 n1 (t * (A1.toReal / A0.toReal)) vProof (Lean source)
theorem kFunctionalSq_map_le {V W : Type*} [AddCommGroup V] [AddCommGroup W] (n0 n1 : V → ℝ≥0∞) (m0 m1 : W → ℝ≥0∞) (D : V →+ W) (A0 A1 : ℝ≥0∞) (hA0 : 0 < A0 ∧ A0 < ⊤) (hA1 : 0 < A1 ∧ A1 < ⊤) (h0 : ∀ v, m0 (D v) ≤ A0 * n0 v) (h1 : ∀ v, m1 (D v) ≤ A1 * n1 v) (t : ℝ) (ht : 0 < t) (v : V) : kFunctionalSq m0 m1 t (D v) ≤ A0 ^ 2 * kFunctionalSq n0 n1 (t * (A1.toReal / A0.toReal)) v := by have hA0z : A0 ≠ 0 := ne_of_gt hA0.1 have hA0t : A0 ≠ ⊤ := ne_of_lt hA0.2 have hA1t : A1 ≠ ⊤ := ne_of_lt hA1.2 have ha0 : 0 < A0.toReal := ENNReal.toReal_pos_iff.mpr hA0 have ha1 : 0 < A1.toReal := ENNReal.toReal_pos_iff.mpr hA1 have hscale : A0 ^ 2 * ofReal ((t * (A1.toReal / A0.toReal)) ^ 2) = ofReal (t ^ 2) * A1 ^ 2 := by rw [mul_pow, ENNReal.ofReal_mul (le_of_lt (sq_pos_of_pos ht)), ENNReal.ofReal_pow (div_nonneg ha1.le ha0.le), ENNReal.ofReal_div_of_pos ha0, ENNReal.ofReal_toReal hA1t, ENNReal.ofReal_toReal hA0t, div_eq_mul_inv, mul_pow, ← ENNReal.inv_pow, ← div_eq_mul_inv] calc A0 ^ 2 * (ofReal (t ^ 2) * (A1 ^ 2 / A0 ^ 2)) = ofReal (t ^ 2) * (A0 ^ 2 * (A1 ^ 2 / A0 ^ 2)) := by ac_rfl _ = _ := by rw [ENNReal.mul_div_cancel (ENNReal.pow_ne_zero hA0z 2) (ENNReal.pow_ne_top hA0t)] unfold kFunctionalSq rw [ENNReal.mul_iInf_of_ne (ENNReal.pow_ne_zero hA0z 2) (ENNReal.pow_ne_top hA0t)] refine le_iInf fun v0 => ?_ rw [ENNReal.mul_iInf_of_ne (ENNReal.pow_ne_zero hA0z 2) (ENNReal.pow_ne_top hA0t)] refine le_iInf fun v1 => ?_ rw [ENNReal.mul_iInf_of_ne (ENNReal.pow_ne_zero hA0z 2) (ENNReal.pow_ne_top hA0t)] refine le_iInf fun h => ?_ have hD : D v = D v0 + D v1 := by rw [h, map_add] refine (iInf_le_of_le (D v0) (iInf_le_of_le (D v1) (iInf_le_of_le hD le_rfl))).trans ?_ calc m0 (D v0) ^ 2 + ofReal (t ^ 2) * m1 (D v1) ^ 2 ≤ (A0 * n0 v0) ^ 2 + ofReal (t ^ 2) * (A1 * n1 v1) ^ 2 := add_le_add (pow_le_pow_left' (h0 v0) 2) (mul_le_mul_right (pow_le_pow_left' (h1 v1) 2) _) _ = A0 ^ 2 * (n0 v0 ^ 2 + ofReal ((t * (A1.toReal / A0.toReal)) ^ 2) * n1 v1 ^ 2) := by rw [mul_add, mul_pow, mul_pow, ← mul_assoc, ← hscale, mul_assoc]
Operators 1 core · 3 supporting Positive endpoint bounds follow by rescaling the K-functional and integrating. ★ exact_interpolation_operators
Exact quadratic operator interpolation
Positive endpoint bounds follow by rescaling the K-functional and integrating. Arbitrary finite nonnegative bounds follow by a limit of positive bounds, using the finite input interpolation norm. The main theorem retains complete endpoint spaces and injective continuous embeddings, matching compatible Banach pairs. No continuity of the ambient linear map beyond the endpoint bounds is required.
Reference: Chandler-Wilde, Hewett, Moiola (2015), Theorem 2.2(i), arXiv:1404.3599v4.
theorem exact_interpolation_operators reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
A common real linear operator from a compatible embedded Banach source pair to an embedded Banach target pair, with finite nonnegative endpoint bounds, satisfies the exact interpolation estimate: the normalized squared interpolation norm of its image in the target pair is at most (A0^(1−θ)·A1^θ)² times the normalized squared interpolation norm of the vector in the source pair, for an interior exponent and a vector with finite interpolation energy.
Formal statement
hypotheses
E0 E1 G0 G1 V W :
i0 :
E0 →L[ℝ] V
i1 :
E1 →L[ℝ] V
j0 :
G0 →L[ℝ] W
j1 :
G1 →L[ℝ] W
hi0 :
Injective i0
hi1 :
Injective i1
D :
V →ₗ[ℝ] W
A0 A1 :
ℝ≥0∞
hA0 :
A0 < ⊤
hA1 :
A1 < ⊤
h0 :
∀ e, embeddedNorm j0 (D (i0 e)) ≤ A0 * ofReal ‖e‖
h1 :
∀ e, embeddedNorm j1 (D (i1 e)) ≤ A1 * ofReal ‖e‖
θ :
ℝ
hθ :
θ ∈ Ioo (0 : ℝ) 1
v :
V
hvfin :
conclusion
Proof (Lean source)
theorem exact_interpolation_operators
(E0 E1 G0 G1 V W : Type*)
[NormedAddCommGroup E0] [NormedSpace ℝ E0] [CompleteSpace E0]
[NormedAddCommGroup E1] [NormedSpace ℝ E1] [CompleteSpace E1]
[NormedAddCommGroup G0] [NormedSpace ℝ G0] [CompleteSpace G0]
[NormedAddCommGroup G1] [NormedSpace ℝ G1] [CompleteSpace G1]
[NormedAddCommGroup V] [NormedSpace ℝ V]
[NormedAddCommGroup W] [NormedSpace ℝ W]
(i0 : E0 →L[ℝ] V) (i1 : E1 →L[ℝ] V)
(j0 : G0 →L[ℝ] W) (j1 : G1 →L[ℝ] W)
(hi0 : Injective i0) (hi1 : Injective i1)
(D : V →ₗ[ℝ] W) (A0 A1 : ℝ≥0∞) (hA0 : A0 < ⊤) (hA1 : A1 < ⊤)
(h0 : ∀ e, embeddedNorm j0 (D (i0 e)) ≤ A0 * ofReal ‖e‖)
(h1 : ∀ e, embeddedNorm j1 (D (i1 e)) ≤ A1 * ofReal ‖e‖)
(θ : ℝ) (hθ : θ ∈ Ioo (0 : ℝ) 1) (v : V)
(hvfin : kNormSq (embeddedNorm i0) (embeddedNorm i1) θ v < ⊤) :
kNormSq (embeddedNorm j0) (embeddedNorm j1) θ (D v) ≤
(rpow A0 (1 - θ) * rpow A1 θ) ^ 2 *
kNormSq (embeddedNorm i0) (embeddedNorm i1) θ v := by
apply le_geometric_of_forall_gt _ _ A0 A1 hvfin hA0 hA1 θ hθ
intro B0 B1 hB0 hB0fin hB1 hB1fin
have hB0pos : 0 < B0 := lt_of_le_of_lt zero_le hB0
have hB1pos : 0 < B1 := lt_of_le_of_lt zero_le hB1
apply kNormSq_map_le_of_pos _ _ _ _ D.toAddMonoidHom B0 B1
⟨hB0pos, hB0fin⟩ ⟨hB1pos, hB1fin⟩ _ _ θ hθ v
· apply embeddedNorm_endpoint_bound_of_pos i0 hi0 D (embeddedNorm j0) B0 hB0pos
intro e
exact (h0 e).trans (mul_le_mul' hB0.le le_rfl)
· apply embeddedNorm_endpoint_bound_of_pos i1 hi1 D (embeddedNorm j1) B1 hB1pos
intro e
exact (h1 e).trans (mul_le_mul' hB1.le le_rfl)
3 supporting declarations (lemmas, instances)
-
kNormSq_map_le_of_postheorem — An additive map with positive finite endpoint bounds has the exact exponent interpolation bound for endpoint gauges, an interior exponent, and any vector.hypothesesV W :n0 n1 :V → ℝ≥0∞m0 m1 :W → ℝ≥0∞D :V →+ WA0 A1 :ℝ≥0∞hA0 :0 < A0 ∧ A0 < ⊤hA1 :0 < A1 ∧ A1 < ⊤h0 :∀ v, m0 (D v) ≤ A0 * n0 vh1 :∀ v, m1 (D v) ≤ A1 * n1 vθ :ℝhθ :θ ∈ Ioo (0 : ℝ) 1v :VProof (Lean source)
theorem kNormSq_map_le_of_pos {V W : Type*} [AddCommGroup V] [AddCommGroup W] (n0 n1 : V → ℝ≥0∞) (m0 m1 : W → ℝ≥0∞) (D : V →+ W) (A0 A1 : ℝ≥0∞) (hA0 : 0 < A0 ∧ A0 < ⊤) (hA1 : 0 < A1 ∧ A1 < ⊤) (h0 : ∀ v, m0 (D v) ≤ A0 * n0 v) (h1 : ∀ v, m1 (D v) ≤ A1 * n1 v) (θ : ℝ) (hθ : θ ∈ Ioo (0 : ℝ) 1) (v : V) : kNormSq m0 m1 θ (D v) ≤ (rpow A0 (1 - θ) * rpow A1 θ) ^ 2 * kNormSq n0 n1 θ v := by have ha0 : 0 < A0.toReal := ENNReal.toReal_pos_iff.mpr hA0 have ha1 : 0 < A1.toReal := ENNReal.toReal_pos_iff.mpr hA1 have hc : 0 < A1.toReal / A0.toReal := div_pos ha1 ha0 have hcoef : A0 ^ 2 * ofReal ((A1.toReal / A0.toReal) ^ (2 * θ)) = (rpow A0 (1 - θ) * rpow A1 θ) ^ 2 := by simp only [ENNReal.rpow_eq_pow] rw [← ENNReal.ofReal_rpow_of_pos hc, ENNReal.ofReal_div_of_pos ha0, ENNReal.ofReal_toReal (ne_of_lt hA1.2), ENNReal.ofReal_toReal (ne_of_lt hA0.2), ENNReal.div_rpow_of_nonneg A1 A0 (by linarith [hθ.1])] calc A0 ^ 2 * (A1 ^ (2 * θ) / A0 ^ (2 * θ)) = (A0 ^ 2 / A0 ^ (2 * θ)) * A1 ^ (2 * θ) := by simp only [div_eq_mul_inv] ac_rfl _ = A0 ^ (2 - 2 * θ) * A1 ^ (2 * θ) := by rw [← ENNReal.rpow_two, ← ENNReal.rpow_sub 2 (2 * θ) (ne_of_gt hA0.1) (ne_of_lt hA0.2)] _ = _ := by rw [mul_pow, ← ENNReal.rpow_two (A0 ^ (1 - θ)), ← ENNReal.rpow_mul, ← ENNReal.rpow_two (A1 ^ θ), ← ENNReal.rpow_mul] congr 1 <;> congr 1 <;> ring unfold kNormSq calc _ ≤ normalizationSq θ * ∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * (A0 ^ 2 * kFunctionalSq n0 n1 (t * (A1.toReal / A0.toReal)) v) := by apply mul_le_mul' le_rfl apply setLIntegral_mono' measurableSet_Ioi intro t ht exact mul_le_mul' le_rfl (kFunctionalSq_map_le n0 n1 m0 m1 D A0 A1 hA0 hA1 h0 h1 t ht v) _ = normalizationSq θ * (A0 ^ 2 * (ofReal ((A1.toReal / A0.toReal) ^ (2 * θ)) * ∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * kFunctionalSq n0 n1 t v)) := by simp_rw [mul_left_comm (ofReal _) (A0 ^ 2)] rw [lintegral_const_mul' _ _ (ENNReal.pow_ne_top (ne_of_lt hA0.2)), lintegral_weighted_dilation _ (measurable_kFunctionalSq_indicator n0 n1 v) _ hc θ] _ = _ := by rw [← hcoef]; ac_rfl -
embeddedNorm_endpoint_bound_of_postheorem — An endpoint estimate on embedded vectors extends to the whole ambient space for an injective embedding, a positive bound, and an ambient map and target gauge. Outside the source endpoint the right side is infinity because A is positive.hypothesesE V W :i :E →L[ℝ] Vhi :D :V → Wm :W → ℝ≥0∞A :ℝ≥0∞hA :0 < Ah :∀ e, m (D (i e)) ≤ A * ofReal ‖e‖v :conclusionm (D v) ≤ A * embeddedNorm i vProof (Lean source)
theorem embeddedNorm_endpoint_bound_of_pos {E V W : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : E →L[ℝ] V) (hi : Injective i) (D : V → W) (m : W → ℝ≥0∞) (A : ℝ≥0∞) (hA : 0 < A) (h : ∀ e, m (D (i e)) ≤ A * ofReal ‖e‖) : ∀ v, m (D v) ≤ A * embeddedNorm i v := by intro v by_cases hv : v ∈ range i · obtain ⟨e, rfl⟩ := hv simpa only [embeddedNorm_apply i hi] using h e · rw [embeddedNorm_eq_top i v hv] simp [ENNReal.mul_top, ne_of_gt hA] -
le_geometric_of_forall_gttheorem — Bounds for every strictly larger positive finite endpoint constant imply the bound at the original finite nonnegative constants, for a finite input energy, a target energy, finite endpoint constants, and an interior exponent.hypothesesProof (Lean source)
theorem le_geometric_of_forall_gt (L K A0 A1 : ℝ≥0∞) (hK : K < ⊤) (hA0 : A0 < ⊤) (hA1 : A1 < ⊤) (θ : ℝ) (hθ : θ ∈ Ioo (0 : ℝ) 1) (h : ∀ B0 B1 : ℝ≥0∞, A0 < B0 → B0 < ⊤ → A1 < B1 → B1 < ⊤ → L ≤ (rpow B0 (1 - θ) * rpow B1 θ) ^ 2 * K) : L ≤ (rpow A0 (1 - θ) * rpow A1 θ) ^ 2 * K := by have hB (A : ℝ≥0∞) : Tendsto (fun ε : ℝ => A + ofReal ε) (𝓝[>] (0 : ℝ)) (𝓝 A) := by have ht : Tendsto (fun ε : ℝ => ε) (𝓝[>] (0 : ℝ)) (𝓝 0) := tendsto_id.mono_left nhdsWithin_le_nhds simpa using (tendsto_const_nhds (x := A)).add (ENNReal.tendsto_ofReal ht) have hp0 := (ENNReal.continuous_rpow_const (y := 1 - θ)).tendsto A0 |>.comp (hB A0) have hp1 := (ENNReal.continuous_rpow_const (y := θ)).tendsto A1 |>.comp (hB A1) have hp : Tendsto (fun ε : ℝ => ((A0 + ofReal ε) ^ (1 - θ) * (A1 + ofReal ε) ^ θ) ^ 2 * K) (𝓝[>] (0 : ℝ)) (𝓝 ((A0 ^ (1 - θ) * A1 ^ θ) ^ 2 * K)) := ENNReal.Tendsto.mul_const ((ENNReal.continuous_pow 2).tendsto _ |>.comp (ENNReal.Tendsto.mul hp0 (inr (ENNReal.rpow_ne_top_of_nonneg hθ.1.le (ne_of_lt hA1))) hp1 (inr (ENNReal.rpow_ne_top_of_nonneg (by linarith [hθ.2]) (ne_of_lt hA0))))) (inr (ne_of_lt hK)) simp only [ENNReal.rpow_eq_pow] at h ⊢ apply ge_of_tendsto hp filter_upwards [self_mem_nhdsWithin] with ε hε exact h _ _ (ENNReal.lt_add_right (ne_of_lt hA0) (ne_of_gt (ENNReal.ofReal_pos.mpr hε))) (ENNReal.add_lt_top.mpr ⟨hA0, ENNReal.ofReal_lt_top⟩) (ENNReal.lt_add_right (ne_of_lt hA1) (ne_of_gt (ENNReal.ofReal_pos.mpr hε))) (ENNReal.add_lt_top.mpr ⟨hA1, ENNReal.ofReal_lt_top⟩)
Pointwise 1 core · 2 supporting Completion of the square for positive real weights and complex scalars provides the pointwise engine for weighted L² interpolation. ★ harmonic_quadratic_iInf
Scalar quadratic minimization
Completion of the square for positive real weights and complex scalars provides the pointwise engine for weighted L² interpolation. This module is independent of the measure-theoretic and embedded-endpoint branches.
theorem harmonic_quadratic_iInf reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
For positive real weights a and b and a complex number z, the infimum of a·|z0|² + b·|z1|² over all decompositions z = z0 + z1 equals a·b/(a+b)·|z|².
Formal statement
Proof (Lean source)
theorem harmonic_quadratic_iInf (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (z : ℂ) :
(⨅ (z0 : ℂ) (z1 : ℂ) (_ : z = z0 + z1),
ofReal (a * ‖z0‖ ^ 2 + b * ‖z1‖ ^ 2)) =
ofReal (a * b / (a + b) * ‖z‖ ^ 2) := by
apply le_antisymm
· obtain ⟨hsum, hvalue⟩ := harmonic_quadratic_attained a b ha hb z
calc
_ ≤ ofReal (a * ‖(b / (a + b)) • z‖ ^ 2 +
b * ‖(a / (a + b)) • z‖ ^ 2) :=
iInf_le_of_le ((b / (a + b)) • z)
(iInf_le_of_le ((a / (a + b)) • z) (iInf_le_of_le hsum le_rfl))
_ = _ := congrArg ofReal hvalue
· refine le_iInf fun z0 => le_iInf fun z1 => le_iInf fun hsum => ?_
apply ENNReal.ofReal_le_ofReal
rw [hsum]
exact harmonic_quadratic_le a b ha hb z0 z1
2 supporting declarations (lemmas, instances)
-
harmonic_quadratic_letheorem — Positive real weights and two complex summands satisfy the harmonic-weight quadratic lower bound.hypothesesa b :ℝha :0 < ahb :0 < bz0 z1 :ℂconclusiona * b / (a + b) * ‖z0 + z1‖ ^ 2 ≤ a * ‖z0‖ ^ 2 + b * ‖z1‖ ^ 2Proof (Lean source)
theorem harmonic_quadratic_le (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (z0 z1 : ℂ) : a * b / (a + b) * ‖z0 + z1‖ ^ 2 ≤ a * ‖z0‖ ^ 2 + b * ‖z1‖ ^ 2 := by have hab : 0 < a + b := add_pos ha hb rw [div_mul_eq_mul_div, div_le_iff₀ hab] simp only [Complex.sq_norm, Complex.normSq_apply, Complex.add_re, Complex.add_im] nlinarith [sq_nonneg (a * z0.re - b * z1.re), sq_nonneg (a * z0.im - b * z1.im)] -
harmonic_quadratic_attainedtheorem — Positive real weights and a complex vector have an explicit minimizing quadratic decomposition. The first summand has coefficient b/(a+b), and the second has coefficient a/(a+b).hypothesesa b :ℝha :0 < ahb :0 < bz :ℂconclusionconclusion 1z = (b / (a + b)) • z + (a / (a + b)) • zconclusion 2a * ‖(b / (a + b)) • z‖ ^ 2 + b * ‖(a / (a + b)) • z‖ ^ 2 = a * b / (a + b) * ‖z‖ ^ 2Proof (Lean source)
theorem harmonic_quadratic_attained (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (z : ℂ) : z = (b / (a + b)) • z + (a / (a + b)) • z ∧ a * ‖(b / (a + b)) • z‖ ^ 2 + b * ‖(a / (a + b)) • z‖ ^ 2 = a * b / (a + b) * ‖z‖ ^ 2 := by have hab : a + b ≠ 0 := ne_of_gt (add_pos ha hb) constructor · rw [← add_smul] have hsum : b / (a + b) + a / (a + b) = 1 := by field_simp ring rw [hsum, one_smul] · simp only [norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] field_simp ring
ScalarIntegral 1 core · 4 supporting The beta integral and Euler reflection formula evaluate the normalization integral exactly. ★ normalized_lintegral_harmonicWeight
Scalar normalization and dilation
The beta integral and Euler reflection formula evaluate the normalization integral exactly. Positive dilation supplies the exponent in the operator estimate. All integration identities are for nonnegative extended integrals, so no nonintegrable-zero convention for a real integral can enter the result.
theorem normalized_lintegral_harmonicWeight reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Positive finite weights and an interior exponent give the identity that the normalization constant times the integral over positive scales t of t^(−1−2θ) times the harmonic weight of a and b at scale t equals a^(1−θ)·b^θ.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem normalized_lintegral_harmonicWeight (a b : ℝ≥0∞)
(ha : 0 < a ∧ a < ⊤) (hb : 0 < b ∧ b < ⊤)
(θ : ℝ) (hθ : θ ∈ Ioo (0 : ℝ) 1) :
normalizationSq θ * (∫⁻ t in Ioi (0 : ℝ),
ofReal (t ^ (-1 - 2 * θ)) * harmonicWeight a b t) =
rpow a (1 - θ) * rpow b θ := by
have hA : 0 < a.toReal := ENNReal.toReal_pos_iff.mpr ha
have hB : 0 < b.toReal := ENNReal.toReal_pos_iff.mpr hb
have haR : ofReal a.toReal = a := ENNReal.ofReal_toReal ha.2.ne
have hbR : ofReal b.toReal = b := ENNReal.ofReal_toReal hb.2.ne
let c : ℝ := sqrt (b.toReal / a.toReal)
have hc : 0 < c := Real.sqrt_pos.mpr (div_pos hB hA)
have hc2 : c ^ 2 = b.toReal / a.toReal := Real.sq_sqrt (div_pos hB hA).le
let F : ℝ → ℝ≥0∞ := fun t => ofReal (t ^ 2 / (1 + t ^ 2))
have hF : Measurable ((Ioi (0 : ℝ)).indicator F) := by
apply Measurable.indicator _ measurableSet_Ioi
dsimp [F]
fun_prop
have hharm : ∀ t : ℝ, harmonicWeight a b t = a * F (t * c) := by
intro t
have hd : 0 < a.toReal + t ^ 2 * b.toReal :=
add_pos_of_pos_of_nonneg hA (mul_nonneg (sq_nonneg t) hB.le)
rw [harmonicWeight, ← haR, ← hbR,
← ENNReal.ofReal_mul (sq_nonneg t),
← ENNReal.ofReal_add hA.le (mul_nonneg (sq_nonneg t) hB.le),
← ENNReal.ofReal_mul hA.le, ← ENNReal.ofReal_div_of_pos hd,
← ENNReal.ofReal_mul hA.le]
congr 1
rw [mul_pow, hc2]
field_simp
have hbase : (∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * F t) =
ofReal (pi / (2 * sin (pi * θ))) := by
rw [← lintegral_quadratic_kernel θ hθ]
apply setLIntegral_congr_fun measurableSet_Ioi
intro t ht
change 0 < t at ht
dsimp [F]
rw [← ENNReal.ofReal_mul (Real.rpow_nonneg ht.le _), ← mul_div_assoc]
congr 1
rw [← Real.rpow_natCast t 2, ← Real.rpow_add ht]
norm_num only [Nat.cast_ofNat]
congr 2
ring
have hscale := lintegral_weighted_dilation F hF c hc θ
have hint : (∫⁻ t in Ioi (0 : ℝ),
ofReal (t ^ (-1 - 2 * θ)) * harmonicWeight a b t) =
a * ofReal (c ^ (2 * θ)) *
ofReal (pi / (2 * sin (pi * θ))) := by
simp_rw [hharm, mul_left_comm (ofReal _) a]
rw [lintegral_const_mul' _ _ ha.2.ne, hscale, hbase, mul_assoc]
have hsin : 0 < sin (pi * θ) :=
Real.sin_pos_of_pos_of_lt_pi (mul_pos Real.pi_pos hθ.1)
(by nlinarith [Real.pi_pos, hθ.2])
have hnorm : normalizationSq θ *
ofReal (pi / (2 * sin (pi * θ))) = 1 := by
rw [normalizationSq, ← ENNReal.ofReal_mul (by positivity)]
have he : (2 * sin (pi * θ) / pi) *
(pi / (2 * sin (pi * θ))) = 1 := by
field_simp
rw [he, ENNReal.ofReal_one]
have hcoeff : a.toReal * c ^ (2 * θ) = a.toReal ^ (1 - θ) * b.toReal ^ θ := by
have hcp : c ^ (2 * θ) = (b.toReal / a.toReal) ^ θ := by
rw [← hc2, ← Real.rpow_natCast_mul hc.le]
norm_num
rw [hcp, Real.div_rpow hB.le hA.le, Real.rpow_sub hA, Real.rpow_one]
ring
rw [hint]
calc
_ = (normalizationSq θ *
ofReal (pi / (2 * sin (pi * θ)))) *
(a * ofReal (c ^ (2 * θ))) := by ring
_ = a * ofReal (c ^ (2 * θ)) := by rw [hnorm, one_mul]
_ = rpow a (1 - θ) * rpow b θ := by
rw [ENNReal.rpow_eq_pow, ENNReal.rpow_eq_pow,
← haR, ← hbR, ENNReal.ofReal_rpow_of_pos hA,
ENNReal.ofReal_rpow_of_pos hB,
← ENNReal.ofReal_mul hA.le,
← ENNReal.ofReal_mul (Real.rpow_nonneg hA.le _), hcoeff]
4 supporting declarations (lemmas, instances)
-
lintegral_beta_reflectiontheorem — An exponent strictly between zero and one gives the reflection-value beta integral on the unit interval.hypothesesp :ℝhp :p ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem lintegral_beta_reflection (p : ℝ) (hp : p ∈ Ioo (0 : ℝ) 1) : (∫⁻ x in Ioo (0 : ℝ) 1, ofReal (x ^ (p - 1) * (1 - x) ^ (-p))) = ofReal (pi / sin (pi * p)) := by let f : ℝ → ℂ := fun x => (x : ℂ) ^ ((p : ℂ) - 1) * (1 - (x : ℂ)) ^ ((1 - (p : ℂ)) - 1) have hconv : IntegrableOn f (Ioo 0 1) := (intervalIntegrable_iff_integrableOn_Ioo_of_le zero_le_one).mp (Complex.betaIntegral_convergent (by simpa using hp.1) (by simp only [Complex.sub_re, Complex.one_re, Complex.ofReal_re]; linarith [hp.2])) have heq : ∀ x ∈ Ioo (0 : ℝ) 1, (f x).re = x ^ (p - 1) * (1 - x) ^ (-p) := by intro x hx simp only [f, ← Complex.ofReal_sub, ← Complex.ofReal_one, ← Complex.ofReal_cpow hx.1.le, ← Complex.ofReal_cpow (sub_pos.mpr hx.2).le, ← Complex.ofReal_mul, Complex.ofReal_re] congr 2 ring have hae : (fun x => (f x).re) =ᵐ[volume.restrict (Ioo 0 1)] (fun x => x ^ (p - 1) * (1 - x) ^ (-p)) := (ae_restrict_mem measurableSet_Ioo).mono heq have hint := hconv.re.congr hae rw [← ofReal_integral_eq_lintegral_ofReal hint ((ae_restrict_mem measurableSet_Ioo).mono (fun x hx => mul_nonneg (Real.rpow_nonneg hx.1.le _) (Real.rpow_nonneg (sub_pos.mpr hx.2).le _)))] have hbeta : Complex.betaIntegral (p : ℂ) (1 - (p : ℂ)) = ((Gamma p * Gamma (1 - p) : ℝ) : ℂ) := by have h := Complex.Gamma_mul_Gamma_eq_betaIntegral (s := (p : ℂ)) (t := 1 - (p : ℂ)) (by simpa using hp.1) (by simp only [Complex.sub_re, Complex.one_re, Complex.ofReal_re]; linarith [hp.2]) rw [show (p : ℂ) + (1 - (p : ℂ)) = 1 by ring, Complex.Gamma_one, one_mul] at h simpa only [ Complex.Gamma_one, one_mul, ← Complex.ofReal_one, ← Complex.ofReal_sub, Complex.Gamma_ofReal, Complex.ofReal_mul] using h.symm have hvalue : (∫ x in Ioo (0 : ℝ) 1, (f x).re) = pi / sin (pi * p) := by have hr : (∫ x in Ioo (0 : ℝ) 1, (f x).re) = (∫ x in Ioo (0 : ℝ) 1, f x).re := integral_re hconv rw [hr] change (∫ x in Ioo (0 : ℝ) 1, f x).re = _ rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le zero_le_one] change (Complex.betaIntegral (p : ℂ) (1 - (p : ℂ))).re = _ rw [hbeta, Complex.ofReal_re, Real.Gamma_mul_Gamma_one_sub] rw [← integral_congr_ae hae, hvalue] -
lintegral_rpow_div_one_add_eq_betatheorem — An exponent strictly between zero and one gives the half-line-to-unit-interval beta substitution.hypothesesp :ℝ_hp :p ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem lintegral_rpow_div_one_add_eq_beta (p : ℝ) (_hp : p ∈ Ioo (0 : ℝ) 1) : (∫⁻ x in Ioi (0 : ℝ), ofReal (x ^ (p - 1) / (1 + x))) = ∫⁻ x in Ioo (0 : ℝ) 1, ofReal (x ^ (p - 1) * (1 - x) ^ (-p)) := by let φ : ℝ → ℝ := fun u => u / (1 - u) have himage : φ '' Ioo (0 : ℝ) 1 = Ioi (0 : ℝ) := by ext x constructor · rintro ⟨u, hu, rfl⟩ exact div_pos hu.1 (sub_pos.mpr hu.2) · intro hx have hd : 0 < 1 + x := by linarith [show 0 < x from hx] refine ⟨x / (1 + x), ⟨div_pos hx hd, (div_lt_one hd).mpr (by linarith)⟩, ?_⟩ dsimp [φ] field_simp ring have hinj : InjOn φ (Ioo (0 : ℝ) 1) := by intro u hu v hv huv dsimp [φ] at huv have h := (div_eq_div_iff (sub_pos.mpr hu.2).ne' (sub_pos.mpr hv.2).ne').mp huv nlinarith have hderiv : ∀ u ∈ Ioo (0 : ℝ) 1, HasDerivWithinAt φ (1 / (1 - u) ^ 2) (Ioo 0 1) u := by intro u hu have h := (hasDerivAt_id u).div ((hasDerivAt_id u).const_sub 1) (sub_pos.mpr hu.2).ne' convert! h.hasDerivWithinAt (s := Ioo (0 : ℝ) 1) using 1 simp [id_eq, sub_add_cancel] rw [← himage, lintegral_image_eq_lintegral_abs_deriv_mul measurableSet_Ioo hderiv hinj] apply setLIntegral_congr_fun measurableSet_Ioo intro u hu have hd : 0 < 1 - u := sub_pos.mpr hu.2 dsimp only rw [abs_of_pos (by positivity : 0 < 1 / (1 - u) ^ 2), ← ENNReal.ofReal_mul (by positivity : 0 ≤ 1 / (1 - u) ^ 2)] congr 1 dsimp [φ] rw [Real.div_rpow hu.1.le hd.le, Real.rpow_sub hd, Real.rpow_one, Real.rpow_neg hd.le] have hpow : (1 - u) ^ p ≠ 0 := (Real.rpow_pos_of_pos hd p).ne' have hadd : 1 + u / (1 - u) = 1 / (1 - u) := by field_simp ring rw [hadd] field_simp -
lintegral_rpow_div_one_addtheorem — An exponent strictly between zero and one gives Euler's positive-half-line beta integral.hypothesesp :ℝhp :p ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem lintegral_rpow_div_one_add (p : ℝ) (hp : p ∈ Ioo (0 : ℝ) 1) : (∫⁻ x in Ioi (0 : ℝ), ofReal (x ^ (p - 1) / (1 + x))) = ofReal (pi / sin (pi * p)) := by rw [lintegral_rpow_div_one_add_eq_beta p hp, lintegral_beta_reflection p hp] -
lintegral_quadratic_kerneltheorem — An exponent strictly between zero and one gives the exact quadratic normalization integral.hypothesesθ :ℝhθ :θ ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem lintegral_quadratic_kernel (θ : ℝ) (hθ : θ ∈ Ioo (0 : ℝ) 1) : (∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (1 - 2 * θ) / (1 + t ^ 2))) = ofReal (pi / (2 * sin (pi * θ))) := by have hp : 1 - θ ∈ Ioo (0 : ℝ) 1 := ⟨by linarith [hθ.2], by linarith [hθ.1]⟩ have himage : (fun t : ℝ => t ^ 2) '' Ioi (0 : ℝ) = Ioi (0 : ℝ) := by ext x constructor · rintro ⟨t, ht, rfl⟩ exact sq_pos_of_pos (show 0 < t from ht) · intro hx exact ⟨Real.sqrt x, Real.sqrt_pos.mpr hx, Real.sq_sqrt hx.le⟩ have hinj : InjOn (fun t : ℝ => t ^ 2) (Ioi (0 : ℝ)) := by intro t ht u hu heq nlinarith [show 0 < t from ht, show 0 < u from hu] have hderiv : ∀ t ∈ Ioi (0 : ℝ), HasDerivWithinAt (fun t : ℝ => t ^ 2) (2 * t) (Ioi 0) t := by intro t ht convert! ((hasDerivAt_id t).pow 2).hasDerivWithinAt (s := Ioi (0 : ℝ)) using 1 simp [id_eq] have hsub := lintegral_image_eq_lintegral_abs_deriv_mul measurableSet_Ioi hderiv hinj (fun x : ℝ => ofReal (x ^ ((1 - θ) - 1) / (1 + x))) rw [himage] at hsub have hkernel : ∀ t ∈ Ioi (0 : ℝ), ofReal (|2 * t|) * ofReal ((t ^ 2) ^ ((1 - θ) - 1) / (1 + t ^ 2)) = ofReal 2 * ofReal (t ^ (1 - 2 * θ) / (1 + t ^ 2)) := by intro t ht change 0 < t at ht rw [abs_of_pos (mul_pos (by norm_num) ht), ← ENNReal.ofReal_mul (by positivity : 0 ≤ 2 * t), ← ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 2)] congr 1 rw [← Real.rpow_natCast_mul ht.le] norm_num only [Nat.cast_ofNat] have he : (2 : ℝ) * (1 - θ - 1) = -2 * θ := by ring rw [he] have hpow : t * t ^ (-2 * θ) = t ^ (1 - 2 * θ) := by simpa only [Real.rpow_one, sub_eq_add_neg, neg_mul] using (Real.rpow_add ht 1 (-2 * θ)).symm rw [mul_assoc, ← mul_div_assoc, hpow] rw [setLIntegral_congr_fun measurableSet_Ioi hkernel, lintegral_const_mul' _ _ ENNReal.ofReal_ne_top, lintegral_rpow_div_one_add (1 - θ) hp] at hsub have hsin : sin (pi * (1 - θ)) = sin (pi * θ) := by rw [mul_sub, mul_one, Real.sin_pi_sub] rw [hsin] at hsub apply (ENNReal.mul_right_inj (by norm_num : ofReal 2 ≠ 0) ENNReal.ofReal_ne_top).mp rw [← hsub, ← ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 2)] congr 1 ring
ScaleIntegral 1 core · 0 supporting Positive dilation of a measurable nonnegative scale function contributes the exact power of the dilation factor in quadratic real interpolation. ★ lintegral_weighted_dilation
Weighted dilation on positive scales
Positive dilation of a measurable nonnegative scale function contributes the exact power of the dilation factor in quadratic real interpolation. Infinite integrals are allowed. This module has no dependence on the scalar normalization evaluation, so the operator branch can use dilation without importing that evaluation.
theorem lintegral_weighted_dilation reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
A nonnegative extended measurable scale function, a positive dilation, and an exponent satisfy the dilation identity: the integral over positive t of t^(−1−2θ)·F(c·t) equals c^(2θ) times the integral over positive t of t^(−1−2θ)·F(t). Only measurability on the positive half-line is required; infinite integrals are allowed.
Formal statement
Proof (Lean source)
theorem lintegral_weighted_dilation (F : ℝ → ℝ≥0∞)
(hF : Measurable (indicator (Ioi (0 : ℝ)) F))
(c : ℝ) (hc : 0 < c) (θ : ℝ) :
(∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * F (t * c)) =
ofReal (c ^ (2 * θ)) *
∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * F t := by
let G : ℝ → ℝ≥0∞ := fun t => ofReal (t ^ (-1 - 2 * θ)) *
(Ioi (0 : ℝ)).indicator F t
have hG : Measurable G :=
((measurable_id.pow_const (-1 - 2 * θ)).ennreal_ofReal).mul hF
have hscale : (∫⁻ t, G (t * c)) =
ofReal c⁻¹ * ∫⁻ t, G t := by
rw [← lintegral_map (μ := volume) (g := fun t : ℝ => t * c) hG (by fun_prop),
Real.map_volume_mul_right hc.ne', lintegral_smul_measure, abs_of_pos (inv_pos.mpr hc)]
rfl
have hweight : ∀ t ∈ Ioi (0 : ℝ),
ofReal (t ^ (-1 - 2 * θ)) * F (t * c) =
ofReal (c ^ (1 + 2 * θ)) * G (t * c) := by
intro t ht
have htc : t * c ∈ Ioi (0 : ℝ) := mul_pos ht hc
simp only [G, indicator_of_mem htc, ← mul_assoc,
← ENNReal.ofReal_mul (Real.rpow_nonneg hc.le _), Real.mul_rpow ht.le hc.le]
have hcancel : c ^ (1 + 2 * θ) * (t ^ (-1 - 2 * θ) * c ^ (-1 - 2 * θ)) =
t ^ (-1 - 2 * θ) := by
rw [mul_left_comm, ← Real.rpow_add hc]
simp
rw [← mul_assoc] at hcancel
rw [hcancel]
have hsupport : (∫⁻ t in Ioi (0 : ℝ), G (t * c)) = ∫⁻ t, G (t * c) := by
rw [← lintegral_indicator measurableSet_Ioi]
congr 1
ext t
by_cases ht : t ∈ Ioi (0 : ℝ)
· simp [ht]
· have htc : t * c ∉ Ioi (0 : ℝ) := by
simpa only [mem_Ioi, mul_pos_iff_of_pos_right hc] using ht
simp [ht, G, htc]
have hbase : (∫⁻ t, G t) =
∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * F t := by
have heq : G = (Ioi (0 : ℝ)).indicator
(fun t => ofReal (t ^ (-1 - 2 * θ)) * F t) := by
ext t
by_cases ht : t ∈ Ioi (0 : ℝ) <;> simp [G, ht]
rw [heq, lintegral_indicator measurableSet_Ioi]
calc
_ = ∫⁻ t in Ioi (0 : ℝ), ofReal (c ^ (1 + 2 * θ)) * G (t * c) :=
setLIntegral_congr_fun measurableSet_Ioi hweight
_ = ofReal (c ^ (1 + 2 * θ)) * ∫⁻ t, G (t * c) := by
rw [lintegral_const_mul' _ _ ENNReal.ofReal_ne_top, hsupport]
_ = _ := by
rw [hscale, ← mul_assoc, ← ENNReal.ofReal_mul (Real.rpow_nonneg hc.le _)]
have hpow : c ^ (1 + 2 * θ) * c⁻¹ = c ^ (2 * θ) := by
rw [show 1 + 2 * θ = 2 * θ + 1 by ring, Real.rpow_add hc, Real.rpow_one]
field_simp
rw [hpow, hbase]
ScaleMeasurability 1 core · 1 supporting Monotonicity on positive scales supplies the measurability needed for dilation. ★ measurable_kFunctionalSq_indicator
Measurability of the scale-dependent K-functional
Monotonicity on positive scales supplies the measurability needed for dilation. The endpoint gauges need not themselves be measurable, since each decomposition cost depends continuously on the scale and the infimum is monotone there.
theorem measurable_kFunctionalSq_indicator reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Arbitrary endpoint gauges and a vector give a measurable K-functional after restriction to positive scales. Use monotoneOn_kFunctionalSq and measurable extension by zero.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem measurable_kFunctionalSq_indicator {V : Type*} [AddCommGroup V]
(n0 n1 : V → ℝ≥0∞) (v : V) :
Measurable (indicator (Ioi (0 : ℝ)) (fun t => kFunctionalSq n0 n1 t v)) := by
apply Monotone.measurable
intro s t hst
by_cases hs : s ∈ Ioi (0 : ℝ)
· have ht : t ∈ Ioi (0 : ℝ) := lt_of_lt_of_le hs hst
simp only [Set.indicator_of_mem hs, Set.indicator_of_mem ht]
exact monotoneOn_kFunctionalSq n0 n1 v hs ht hst
· simp only [Set.indicator_of_notMem hs]
exact zero_le
1 supporting declaration (lemmas, instances)
-
monotoneOn_kFunctionalSqtheorem — Arbitrary endpoint gauges and a vector give a monotone squared K-functional on positive scales.hypothesesconclusionProof (Lean source)
theorem monotoneOn_kFunctionalSq {V : Type*} [AddCommGroup V] (n0 n1 : V → ℝ≥0∞) (v : V) : MonotoneOn (fun t => kFunctionalSq n0 n1 t v) (Ioi (0 : ℝ)) := by intro s hs t ht hst unfold kFunctionalSq refine iInf_mono fun v0 => iInf_mono fun v1 => iInf_mono fun _ => ?_ exact add_le_add le_rfl (mul_le_mul' (ENNReal.ofReal_le_ofReal (pow_le_pow_left₀ (le_of_lt hs) hst 2)) le_rfl)
SupportedTonelli 1 core · 0 supporting A jointly measurable nonnegative kernel can be integrated in either order when one measure is s-finite and the other is sigma-finite on a set containing the kernel's support. ★ lintegral_lintegral_swap_of_sigmaFinite_support
Tonelli on sigma-finite support
A jointly measurable nonnegative kernel can be integrated in either order when one measure is s-finite and the other is sigma-finite on a set containing the kernel's support. The ambient second measure may be arbitrary. This is a support restriction wrapper around Mathlib's Tonelli theorem, retaining infinite values.
theorem lintegral_lintegral_swap_of_sigmaFinite_support reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
A jointly measurable nonnegative kernel that vanishes outside a fixed set in its second variable admits interchange of its two integrals, for an s-finite first measure and a second measure sigma-finite on that set.
Formal statement
hypotheses
T S :
μ :
Measure S
s :
Set S
SigmaFinite (μ.restrict s)
F :
T × S → ℝ≥0∞
hF :
hzero :
∀ t x
if
x ∉ s
then
F (t, x) = 0
conclusion
(∫⁻ t, ∫⁻ x, F (t, x) ∂μ ∂ν) = ∫⁻ x, ∫⁻ t, F (t, x) ∂ν ∂μ
Proof (Lean source)
theorem lintegral_lintegral_swap_of_sigmaFinite_support
{T S : Type*} [MeasurableSpace T] [MeasurableSpace S]
(ν : Measure T) [SFinite ν] (μ : Measure S) (s : Set S)
[SigmaFinite (μ.restrict s)] (F : T × S → ℝ≥0∞)
(hF : Measurable F) (hzero : ∀ t x, x ∉ s → F (t, x) = 0) :
(∫⁻ t, ∫⁻ x, F (t, x) ∂μ ∂ν) = ∫⁻ x, ∫⁻ t, F (t, x) ∂ν ∂μ := by
have hrestrict (t : T) : (∫⁻ x in s, F (t, x) ∂μ) = ∫⁻ x, F (t, x) ∂μ := by
apply setLIntegral_eq_of_support_subset
intro x hx
by_contra hxs
exact hx (hzero t x hxs)
calc
_ = ∫⁻ t, ∫⁻ x in s, F (t, x) ∂μ ∂ν := by simp_rw [hrestrict]
_ = ∫⁻ x in s, ∫⁻ t, F (t, x) ∂ν ∂μ :=
lintegral_lintegral_swap hF.aemeasurable
_ = _ := by
apply setLIntegral_eq_of_support_subset
intro x hx
by_contra hxs
exact hx (by simp [hzero _ x hxs])
Weighted 1 core · 1 supporting Pointwise quadratic minimization gives the harmonic-weight K-functional. ★ weighted_l2_interpolation
Exact normalized interpolation of weighted L² spaces
Pointwise quadratic minimization gives the harmonic-weight K-functional. The endpoint-sum hypothesis supplies sigma-finite support, sufficient for Tonelli on an arbitrary declared measure space. Scalar kernel evaluation then gives exactly the geometric-weight energy, including infinite energies. Neither uniform bounds on the weights nor a global sigma-finiteness assumption is used.
Reference: Chandler-Wilde, Hewett, Moiola (2015), Theorem 3.1, arXiv:1404.3599v4.
theorem weighted_l2_interpolation reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Positive finite almost-everywhere measurable endpoint weights give exact equality of normalized quadratic interpolation energy and geometric-weight L² energy, for an interior exponent and a function in the endpoint sum, on any measure space.
Formal statement
hypotheses
S :
Type*
μ :
Measure S
w0 w1 :
S → ℝ≥0∞
hw0 :
Measurable w0
hw1 :
Measurable w1
hw :
∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤
θ :
ℝ
hθ :
θ ∈ Ioo (0 : ℝ) 1
f :
S →ₘ[μ] ℂ
Proof (Lean source)
theorem weighted_l2_interpolation {S : Type*} [MeasurableSpace S]
(μ : Measure S) (w0 w1 : S → ℝ≥0∞)
(hw0 : Measurable w0) (hw1 : Measurable w1)
(hw : ∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤)
(θ : ℝ) (hθ : θ ∈ Ioo (0 : ℝ) 1) (f : S →ₘ[μ] ℂ)
(hf : ∃ f0 f1 : S →ₘ[μ] ℂ, f = f0 + f1 ∧
wNorm w0 μ f0 < ⊤ ∧ wNorm w1 μ f1 < ⊤) :
kNormSq (wNorm w0 μ) (wNorm w1 μ) θ f =
∫⁻ x, rpow (w0 x) (1 - θ) * rpow (w1 x) θ *
(‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ := by
unfold kNormSq
rw [setLIntegral_congr_fun measurableSet_Ioi
(fun t ht => congrArg (fun z => ofReal (t ^ (-1 - 2 * θ)) * z)
(kFunctionalSq_wNorm μ w0 w1 hw0 hw1 hw t ht f))]
rw [lintegral_harmonic_energy_comm μ w0 w1 hw0 hw1 hw θ f hf,
← lintegral_const_mul' (normalizationSq θ) _ ENNReal.ofReal_ne_top]
apply lintegral_congr_ae
filter_upwards [hw] with x hx
rw [← mul_assoc, normalized_lintegral_harmonicWeight
(w0 x) (w1 x) ⟨hx.1, hx.2.1⟩ ⟨hx.2.2.1, hx.2.2.2⟩ θ hθ]
1 supporting declaration (lemmas, instances)
-
lintegral_harmonic_energy_commtheorem — A function with a finite endpoint-sum decomposition under positive finite measurable weights allows interchange of the harmonic-kernel integrals, for any exponent and any declared measure.hypothesesS :Type*μ :Measure Sw0 w1 :S → ℝ≥0∞hw0 :Measurable w0hw1 :Measurable w1hw :∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤θ :ℝf :S →ₘ[μ] ℂconclusion(∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * ∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ)= ∫⁻ x, (∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * harmonicWeight (w0 x) (w1 x) t) * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μProof (Lean source)
theorem lintegral_harmonic_energy_comm {S : Type*} [MeasurableSpace S] (μ : Measure S) (w0 w1 : S → ℝ≥0∞) (hw0 : Measurable w0) (hw1 : Measurable w1) (hw : ∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤) (θ : ℝ) (f : S →ₘ[μ] ℂ) (hf : ∃ f0 f1 : S →ₘ[μ] ℂ, f = f0 + f1 ∧ wNorm w0 μ f0 < ⊤ ∧ wNorm w1 μ f1 < ⊤) : (∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * ∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ) = ∫⁻ x, (∫⁻ t in Ioi (0 : ℝ), ofReal (t ^ (-1 - 2 * θ)) * harmonicWeight (w0 x) (w1 x) t) * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ := by have := sigmaFinite_restrict_support_of_endpoint_sum μ w0 w1 hw0 hw1 hw f hf let F : ℝ × S → ℝ≥0∞ := fun p => ofReal (p.1 ^ (-1 - 2 * θ)) * harmonicWeight (w0 p.2) (w1 p.2) p.1 * (‖f p.2‖₊ : ℝ≥0∞) ^ 2 have hp : Measurable (fun p : ℝ × S => ofReal (p.1 ^ (-1 - 2 * θ))) := (measurable_fst.pow measurable_const).ennreal_ofReal have ht : Measurable (fun p : ℝ × S => ofReal (p.1 ^ 2)) := (measurable_fst.pow_const 2).ennreal_ofReal have h0 := hw0.comp (measurable_snd : Measurable (Prod.snd : ℝ × S → S)) have h1 := hw1.comp (measurable_snd : Measurable (Prod.snd : ℝ × S → S)) have hH : Measurable (fun p : ℝ × S => harmonicWeight (w0 p.2) (w1 p.2) p.1) := (h0.mul (ht.mul h1)).div (h0.add (ht.mul h1)) have hF : Measurable F := (hp.mul hH).mul ((f.measurable.comp measurable_snd).enorm.pow_const 2) have hzero : ∀ t x, x ∉ {x | f x ≠ 0} → F (t, x) = 0 := by intro t x hx have hx0 : f x = 0 := by simpa using hx simp [F, hx0] have hswap := lintegral_lintegral_swap_of_sigmaFinite_support (volume.restrict (Ioi (0 : ℝ))) μ {x | f x ≠ 0} F hF hzero calc _ = ∫⁻ t in Ioi (0 : ℝ), ∫⁻ x, F (t, x) ∂μ := by apply lintegral_congr intro t rw [← lintegral_const_mul' _ _ ENNReal.ofReal_ne_top] simp only [F, mul_assoc] _ = ∫⁻ x, (∫⁻ t in Ioi (0 : ℝ), F (t, x)) ∂μ := hswap _ = _ := by apply lintegral_congr intro x exact lintegral_mul_const' ((‖f x‖₊ : ℝ≥0∞) ^ 2) (fun t => ofReal (t ^ (-1 - 2 * θ)) * harmonicWeight (w0 x) (w1 x) t) (by finiteness)
WeightedMinimum 1 core · 2 supporting Pointwise completion of the square gives a lower bound for every decomposition and an explicit measurable minimizing decomposition. ★ kFunctionalSq_wNorm
The quadratic K-functional of weighted L² spaces
Pointwise completion of the square gives a lower bound for every decomposition and an explicit measurable minimizing decomposition. Their combination evaluates the K-functional as harmonic-weight energy on any measure space, even when the energy is infinite. Scalar normalization and Tonelli are separate later layers.
theorem kFunctionalSq_wNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Measurable weights that are positive finite almost everywhere give the harmonic-weight formula for the squared K-functional of any measurable function modulo null sets, at a positive scale. Combine the preceding lower bound and attained upper bound by the infimum rules.
Formal statement
hypotheses
S :
Type*
μ :
Measure S
w0 w1 :
S → ℝ≥0∞
hw0 :
Measurable w0
hw1 :
Measurable w1
hw :
∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤
t :
ℝ
ht :
0 < t
f :
S →ₘ[μ] ℂ
conclusion
= ∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ
Proof (Lean source)
theorem kFunctionalSq_wNorm {S : Type*} [MeasurableSpace S]
(μ : Measure S) (w0 w1 : S → ℝ≥0∞)
(hw0 : Measurable w0) (hw1 : Measurable w1)
(hw : ∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤)
(t : ℝ) (ht : 0 < t) (f : S →ₘ[μ] ℂ) :
kFunctionalSq (wNorm w0 μ) (wNorm w1 μ) t f =
∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ := by
apply le_antisymm
· obtain ⟨f0, f1, hf, he⟩ := exists_harmonic_minimizer μ w0 w1 hw0 hw1 hw t ht f
unfold kFunctionalSq
exact iInf_le_of_le f0 (iInf_le_of_le f1 (iInf_le_of_le hf he.le))
· unfold kFunctionalSq
refine le_iInf fun f0 => le_iInf fun f1 => le_iInf fun hf => ?_
exact harmonic_energy_le_cost μ w0 w1 hw0 hw t ht f f0 f1 hf
2 supporting declarations (lemmas, instances)
-
harmonic_energy_le_costtheorem — Two weights, the first of them measurable, that are positive finite almost everywhere give a pointwise-minimum lower bound on each decomposition's quadratic weighted energy, at a positive scale for a decomposition modulo null sets. Use wNorm_sq, the almost-everywhere addition rule, harmonic_quadratic_le, and monotonicity and addition of nonnegative integrals.hypothesesS :Type*μ :Measure Sw0 w1 :S → ℝ≥0∞hw0 :Measurable w0hw :∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤t :ℝht :0 < tf f0 f1 :S →ₘ[μ] ℂhf :f = f0 + f1conclusion(∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ)Proof (Lean source)
theorem harmonic_energy_le_cost {S : Type*} [MeasurableSpace S] (μ : Measure S) (w0 w1 : S → ℝ≥0∞) (hw0 : Measurable w0) (hw : ∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤) (t : ℝ) (ht : 0 < t) (f f0 f1 : S →ₘ[μ] ℂ) (hf : f = f0 + f1) : (∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ) ≤ wNorm w0 μ f0 ^ 2 + ofReal (t ^ 2) * wNorm w1 μ f1 ^ 2 := by rw [cost_integral μ w0 w1 hw0 t f0 f1] apply lintegral_mono_ae filter_upwards [hw, AEEqFun.coeFn_add f0 f1] with x hx hadd have ha : 0 < (w0 x).toReal := ENNReal.toReal_pos_iff.mpr ⟨hx.1, hx.2.1⟩ have hb : 0 < t ^ 2 * (w1 x).toReal := mul_pos (sq_pos_of_pos ht) (ENNReal.toReal_pos_iff.mpr ⟨hx.2.2.1, hx.2.2.2⟩) have h := ENNReal.ofReal_le_ofReal (harmonic_quadratic_le _ _ ha hb (f0 x) (f1 x)) rw [ENNReal.ofReal_add (mul_nonneg ha.le (sq_nonneg _)) (mul_nonneg hb.le (sq_nonneg _)), ofReal_energy _ ha.le, ofReal_energy _ hb.le, ENNReal.ofReal_mul (sq_nonneg t), ENNReal.ofReal_toReal hx.2.1.ne, ENNReal.ofReal_toReal hx.2.2.2.ne, ofReal_energy _ (div_nonneg (mul_nonneg ha.le hb.le) (add_nonneg ha.le hb.le))] at h rw [harmonicWeight_real _ _ hx.2.1 hx.2.2.2 hx.1 hx.2.2.1 t ht, hf, hadd] simpa only [mul_assoc, Pi.add_apply] using h -
exists_harmonic_minimizertheorem — Measurable weights that are positive finite almost everywhere give a measurable minimizing decomposition of any measurable complex function modulo null sets, at a positive scale.hypothesesS :Type*μ :Measure Sw0 w1 :S → ℝ≥0∞hw0 :Measurable w0hw1 :Measurable w1hw :∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤t :ℝht :0 < tf :S →ₘ[μ] ℂconclusion∃ f0 f1 : S →ₘ[μ] ℂ,conclusion 1f = f0 + f1conclusion 2= ∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μProof (Lean source)
theorem exists_harmonic_minimizer {S : Type*} [MeasurableSpace S] (μ : Measure S) (w0 w1 : S → ℝ≥0∞) (hw0 : Measurable w0) (hw1 : Measurable w1) (hw : ∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤) (t : ℝ) (ht : 0 < t) (f : S →ₘ[μ] ℂ) : ∃ f0 f1 : S →ₘ[μ] ℂ, f = f0 + f1 ∧ wNorm w0 μ f0 ^ 2 + ofReal (t ^ 2) * wNorm w1 μ f1 ^ 2 = ∫⁻ x, harmonicWeight (w0 x) (w1 x) t * (‖f x‖₊ : ℝ≥0∞) ^ 2 ∂μ := by let a : S → ℝ := fun x => (w0 x).toReal let b : S → ℝ := fun x => t ^ 2 * (w1 x).toReal have hma : Measurable a := hw0.ennreal_toReal have hmb : Measurable b := measurable_const.mul hw1.ennreal_toReal let g0 : S → ℂ := fun x => (b x / (a x + b x)) • f x let g1 : S → ℂ := fun x => (a x / (a x + b x)) • f x have hm0 : AEStronglyMeasurable g0 μ := ((hmb.div (hma.add hmb)).aestronglyMeasurable).smul f.aestronglyMeasurable have hm1 : AEStronglyMeasurable g1 μ := ((hma.div (hma.add hmb)).aestronglyMeasurable).smul f.aestronglyMeasurable let f0 : S →ₘ[μ] ℂ := AEEqFun.mk g0 hm0 let f1 : S →ₘ[μ] ℂ := AEEqFun.mk g1 hm1 have he0 : f0 =ᵐ[μ] g0 := AEEqFun.coeFn_mk g0 hm0 have he1 : f1 =ᵐ[μ] g1 := AEEqFun.coeFn_mk g1 hm1 refine ⟨f0, f1, ?_, ?_⟩ · apply AEEqFun.ext filter_upwards [hw, he0, he1, AEEqFun.coeFn_add f0 f1] with x hx h0 h1 hadd have ha : 0 < a x := ENNReal.toReal_pos_iff.mpr ⟨hx.1, hx.2.1⟩ have hb : 0 < b x := mul_pos (sq_pos_of_pos ht) (ENNReal.toReal_pos_iff.mpr ⟨hx.2.2.1, hx.2.2.2⟩) rw [hadd] change f x = f0 x + f1 x rw [h0, h1] exact (harmonic_quadratic_attained _ _ ha hb (f x)).1 · rw [cost_integral μ w0 w1 hw0 t f0 f1] apply lintegral_congr_ae filter_upwards [hw, he0, he1] with x hx h0 h1 have ha : 0 < a x := ENNReal.toReal_pos_iff.mpr ⟨hx.1, hx.2.1⟩ have hb : 0 < b x := mul_pos (sq_pos_of_pos ht) (ENNReal.toReal_pos_iff.mpr ⟨hx.2.2.1, hx.2.2.2⟩) have h := congrArg ofReal (harmonic_quadratic_attained _ _ ha hb (f x)).2 rw [ENNReal.ofReal_add (mul_nonneg ha.le (sq_nonneg _)) (mul_nonneg hb.le (sq_nonneg _)), ofReal_energy _ ha.le, ofReal_energy _ hb.le, ofReal_energy _ (div_nonneg (mul_nonneg ha.le hb.le) (add_nonneg ha.le hb.le))] at h dsimp only [a, b] at h rw [ENNReal.ofReal_mul (sq_nonneg t), ENNReal.ofReal_toReal hx.2.1.ne, ENNReal.ofReal_toReal hx.2.2.2.ne] at h rw [harmonicWeight_real _ _ hx.2.1 hx.2.2.2 hx.1 hx.2.2.1 t ht, h0, h1] simpa only [g0, g1, a, b, mul_assoc] using h
WeightedSupport 1 core · 1 supporting A finite nonnegative integral controls the measure of positive superlevel sets. ★ sigmaFinite_restrict_support_of_endpoint_sum
Sigma-finite support from finite weighted energy
A finite nonnegative integral controls the measure of positive superlevel sets. Exhausting by these sets gives sigma-finite measure wherever the density is positive almost everywhere. Applying this fact to the sum of two finite endpoint energy densities gives sigma-finite support of an endpoint-sum function, even when the ambient measure space is arbitrary.
theorem sigmaFinite_restrict_support_of_endpoint_sum reviewed
⚑ flagged
Causalean.Mathlib.Analysis.RealInterpolation
Let μ be a measure and let two measurable weights w0 and w1 be positive and finite μ-almost everywhere. If a complex function f, defined up to μ-null sets, splits as a sum of two pieces whose weighted L² norms under w0 and w1 respectively are finite, then μ restricted to the set where f is nonzero is σ-finite.
Formal statement
hypotheses
S :
Type*
μ :
Measure S
w0 w1 :
S → ℝ≥0∞
hw0 :
Measurable w0
hw1 :
Measurable w1
hw :
∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤
f :
S →ₘ[μ] ℂ
conclusion
SigmaFinite (μ.restrict {x | f x ≠ 0})
Proof (Lean source)
theorem sigmaFinite_restrict_support_of_endpoint_sum {S : Type*} [MeasurableSpace S]
(μ : Measure S) (w0 w1 : S → ℝ≥0∞)
(hw0 : Measurable w0) (hw1 : Measurable w1)
(hw : ∀ᵐ x ∂μ, 0 < w0 x ∧ w0 x < ⊤ ∧ 0 < w1 x ∧ w1 x < ⊤)
(f : S →ₘ[μ] ℂ)
(hf : ∃ f0 f1 : S →ₘ[μ] ℂ, f = f0 + f1 ∧
wNorm w0 μ f0 < ⊤ ∧ wNorm w1 μ f1 < ⊤) :
SigmaFinite (μ.restrict {x | f x ≠ 0}) := by
obtain ⟨f0, f1, hsum, hfin0, hfin1⟩ := hf
let g0 : S → ℝ≥0∞ := fun x => w0 x * (‖f0 x‖₊ : ℝ≥0∞) ^ 2
let g1 : S → ℝ≥0∞ := fun x => w1 x * (‖f1 x‖₊ : ℝ≥0∞) ^ 2
have hg0 : Measurable g0 := hw0.mul (f0.measurable.enorm.pow_const 2)
have hg1 : Measurable g1 := hw1.mul (f1.measurable.enorm.pow_const 2)
apply sigmaFinite_restrict_of_ae_pos_of_lintegral_lt_top μ {x | f x ≠ 0}
(f.measurable (measurableSet_singleton 0) |>.compl) (fun x => g0 x + g1 x)
(hg0.add hg1)
· filter_upwards [hw, AEEqFun.coeFn_add f0 f1] with x hx hadd
intro hfx
have hsumx : f x = f0 x + f1 x := by simpa only [hsum, Pi.add_apply] using hadd
have hpos (w : ℝ≥0∞) (hwpos : 0 < w) (z : ℂ) (hz : z ≠ 0) :
0 < w * (‖z‖₊ : ℝ≥0∞) ^ 2 := by
have hnorm : 0 < ‖z‖₊ := nnnorm_pos.mpr hz
positivity
by_cases h0 : f0 x = 0
· have h1 : f1 x ≠ 0 := by simpa [hsumx, h0] using hfx
exact (hpos _ hx.2.2.1 _ h1).trans_le (le_add_left le_rfl)
· exact (hpos _ hx.1 _ h0).trans_le (le_add_right le_rfl)
· rw [lintegral_add_left hg0]
change (∫⁻ x, w0 x * (‖f0 x‖₊ : ℝ≥0∞) ^ 2 ∂μ) +
(∫⁻ x, w1 x * (‖f1 x‖₊ : ℝ≥0∞) ^ 2 ∂μ) < ⊤
rw [← wNorm_sq, ← wNorm_sq]
exact ENNReal.add_lt_top.mpr ⟨ENNReal.pow_lt_top hfin0, ENNReal.pow_lt_top hfin1⟩
1 supporting declaration (lemmas, instances)
-
sigmaFinite_restrict_of_ae_pos_of_lintegral_lt_toptheorem — A measurable nonnegative density with finite integral that is positive almost everywhere on a measurable set gives sigma-finite measure on that set for any ambient measure.hypothesesS :Type*μ :Measure Ss :Set Shs :g :S → ℝ≥0∞hg :hpos :∀ᵐ x ∂μ, x ∈ s → 0 < g xhfin :(∫⁻ x, g x ∂μ) < ⊤conclusionSigmaFinite (μ.restrict s)Proof (Lean source)
theorem sigmaFinite_restrict_of_ae_pos_of_lintegral_lt_top {S : Type*} [MeasurableSpace S] (μ : Measure S) (s : Set S) (hs : MeasurableSet s) (g : S → ℝ≥0∞) (hg : Measurable g) (hpos : ∀ᵐ x ∂μ, x ∈ s → 0 < g x) (hfin : (∫⁻ x, g x ∂μ) < ⊤) : SigmaFinite (μ.restrict s) := by have hzero : (μ.restrict s) {x | g x = 0} = 0 := by have hpos' : ∀ᵐ x ∂μ.restrict s, 0 < g x := (ae_restrict_iff' hs).2 hpos simpa only [ae_iff, not_lt, nonpos_iff_eq_zero] using hpos' let c : ℕ → ℝ≥0∞ := fun n => ((n + 1 : ℕ) : ℝ≥0∞)⁻¹ have hc0 (n : ℕ) : c n ≠ 0 := ENNReal.inv_ne_zero.mpr (ENNReal.natCast_ne_top _) have hctop (n : ℕ) : c n ≠ ⊤ := by simp [c] have hfinite (n : ℕ) : (μ.restrict s) {x | c n ≤ g x} < ⊤ := lt_of_le_of_lt ((Measure.restrict_apply_le _ _).trans (meas_ge_le_lintegral_div hg.aemeasurable (hc0 n) (hctop n))) (ENNReal.div_lt_top hfin.ne (hc0 n)) apply sigmaFinite_iff.mpr refine ⟨{ set := fun n => {x | c n ≤ g x} ∪ {x | g x = 0} set_mem := fun _ => mem_univ _ finite := fun n => ?_ spanning := ?_ }⟩ · exact lt_of_le_of_lt (measure_union_le _ _) (by simpa [hzero] using hfinite n) · apply eq_univ_of_forall intro x by_cases hx : g x = 0 · exact mem_iUnion.mpr ⟨0, inr hx⟩ · obtain ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt hx refine mem_iUnion.mpr ⟨n, inl ?_⟩ exact (ENNReal.inv_le_inv.mpr (by exact_mod_cast le_succ n)).trans hn.le