Lean4
/-- The main inductive step in the grid-lines lemma for the Gagliardo-Nirenberg-Sobolev inequality.
The grid-lines operation `GridLines.T` on a nonnegative function on a finitary product type is
less than or equal to the grid-lines operation of its partial integral in one co-ordinate
(the latter intuitively considered as a function on a space "one dimension down"). -/
theorem T_insert_le_T_lmarginal_singleton [∀ i, SigmaFinite (μ i)] (hp₀ : 0 ≤ p) (s : Finset ι)
(hp : (s.card : ℝ) * p ≤ 1) (i : ι) (hi : i ∉ s) {f : (∀ i, A i) → ℝ≥0∞} (hf : Measurable f) :
T μ p f (insert i s) ≤ T μ p (∫⋯∫⁻_{ i }, f ∂μ) s := by
/- The proof is a tricky computation that relies on Hölder's inequality at its heart.
The left-hand-side is an `|s|+1`-times iterated integral. Let `xᵢ` denote the `i`-th variable.
We first push the integral over the `i`-th variable as the
innermost integral. This is done in a single step with `MeasureTheory.lmarginal_insert'`,
but in fact hides a repeated application of Fubini's theorem.
The integrand is a product of `|s|+2` factors, in `|s|+1` of them we integrate over one
additional variable. We split of the factor that integrates over `xᵢ`,
and apply Hölder's inequality to the remaining factors (whose powers sum exactly to 1).
After reordering factors, and combining two factors into one we obtain the right-hand side. -/
calc
T μ p f (insert i s) = ∫⋯∫⁻_insert i s, f ^ (1 - (s.card : ℝ) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{ j }, f ∂μ) ^ p ∂μ :=
by
-- unfold `T` and reformulate the exponents
simp_rw [T, card_insert_of_notMem hi]
congr!
push_cast
ring
_ =
∫⋯∫⁻_s,
(fun x ↦
∫⁻ (t : A i),
(f (update x i t) ^ (1 - (s.card : ℝ) * p) *
∏ j ∈ insert i s, (∫⋯∫⁻_{ j }, f ∂μ) (update x i t) ^ p) ∂(μ i)) ∂μ :=
by
-- pull out the integral over `xᵢ`
rw [lmarginal_insert' _ _ hi]
· simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
· change Measurable (fun x ↦ _)
simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
refine (hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_
exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _
_ ≤ T μ p (∫⋯∫⁻_{ i }, f ∂μ) s :=
lmarginal_mono (s := s)
(fun x ↦ ?_)
-- The remainder of the computation happens within an `|s|`-fold iterated integral
simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
set X := update x i
have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{ j }, f ∂μ) (X t) := fun {_} ↦
hf.lmarginal μ |>.comp <| measurable_update _
have hF₀ : Measurable fun t ↦ f (X t) := hf.comp <| measurable_update _
let k : ℝ := s.card
have hk' : 0 ≤ 1 - k * p := by linarith only [hp]
calc
∫⁻ t, f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{ j }, f ∂μ) (X t) ^ p ∂(μ i) =
∫⁻ t, (∫⋯∫⁻_{ i }, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, ((∫⋯∫⁻_{ j }, f ∂μ) (X t) ^ p)) ∂(μ i) :=
by
-- rewrite integrand so that `(∫⋯∫⁻_insert i s, f ∂μ) ^ p` comes first
clear_value X
congr! 2 with t
simp_rw [prod_insert hi]
ring_nf
_ = (∫⋯∫⁻_{ i }, f ∂μ) x ^ p * ∫⁻ t, f (X t) ^ (1 - k * p) * ∏ j ∈ s, ((∫⋯∫⁻_{ j }, f ∂μ) (X t)) ^ p ∂(μ i) := by
-- pull out this constant factor
have : ∀ t, (∫⋯∫⁻_{ i }, f ∂μ) (X t) = (∫⋯∫⁻_{ i }, f ∂μ) x :=
by
intro t
rw [lmarginal_update_of_mem]
exact Iff.mpr Finset.mem_singleton rfl
simp_rw [this]
rw [lintegral_const_mul]
exact (hF₀.pow_const _).mul <| Finset.measurable_fun_prod _ fun _ _ ↦ hF₁.pow_const _
_ ≤
(∫⋯∫⁻_{ i }, f ∂μ) x ^ p *
((∫⁻ t, f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ t, (∫⋯∫⁻_{ j }, f ∂μ) (X t) ∂μ i) ^ p) :=
by
-- apply Hölder's inequality
gcongr
apply ENNReal.lintegral_mul_prod_norm_pow_le
· exact hF₀.aemeasurable
· intros
exact hF₁.aemeasurable
· simp only [sum_const, nsmul_eq_mul]
ring
· exact hk'
· exact fun _ _ ↦ hp₀
_ = (∫⋯∫⁻_{ i }, f ∂μ) x ^ p * ((∫⋯∫⁻_{ i }, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{ i, j }, f ∂μ) x ^ p) := by
-- absorb the newly-created integrals into `∫⋯∫`
congr! 2
· rw [lmarginal_singleton]
refine prod_congr rfl fun j hj => ?_
have hi' : i ∉ ({ j } : Finset ι) :=
by
simp only [Finset.mem_singleton] at hj ⊢
exact fun h ↦ hi (h ▸ hj)
rw [lmarginal_insert _ hf hi']
_ = (∫⋯∫⁻_{ i }, f ∂μ) x ^ (p + (1 - k * p)) * ∏ j ∈ s, (∫⋯∫⁻_{ i, j }, f ∂μ) x ^ p := by
-- combine two `(∫⋯∫⁻_insert i s, f ∂μ) x` terms
rw [ENNReal.rpow_add_of_nonneg]
· ring
· exact hp₀
· exact hk'
_ ≤ (∫⋯∫⁻_{ i }, f ∂μ) x ^ (1 - (s.card - 1 : ℝ) * p) * ∏ j ∈ s, (∫⋯∫⁻_{ j }, (∫⋯∫⁻_{ i }, f ∂μ) ∂μ) x ^ p := by
-- identify the result with the RHS integrand
congr! 2 with j hj
· ring
· congr! 1
rw [← lmarginal_union μ f hf]
· congr
rw [Finset.union_comm]
rfl
· rw [Finset.disjoint_singleton]
simp only at hj
exact fun h ↦ hi (h ▸ hj)
