PL1/EnfloIntrinsic.lean

All source files · Download exact source

SHA-256: d0aa35913a4370aecf55a8589305bcb9e3be9690917250d6fc5d8afcba6218ca

1import PL1.EnfloVanishing2import PL1.EnfloSum3import PL1.DyadicProjection45/-! Intrinsic weighted defects force dyadic maximum decay in every graph coordinate. -/67noncomputable section8set_option backward.isDefEq.respectTransparency false9open MeasureTheory Filter10open scoped BigOperators Topology ENNReal NNReal1112namespace PL1.EnfloBush13open IntrinsicGraph ResolventEstimates1415variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)16variable (S : DyadicSystem ℝ (Lp ℝ 1 μ))1718theorem norm_intrinsic_coord_le (n : ℕ) (x : S.IntrinsicSpace) :19    ‖coord S.analysis n x‖ ≤ ‖x‖ :=20  lp.norm_apply_le_norm (by simp) (x : IntrinsicGraph.Ambient (Y := Lp ℝ 1 μ)) n2122theorem intrinsic_defect_eq (n : ℕ) (x : S.IntrinsicSpace) :23    evalZero S.analysis x - S.operator (n + 1) (evalZero S.analysis x) =24      dyadicRatio ^ (n + 1) • coord S.analysis (n + 1) x := by25  rw [coord_eq]26  change _ = dyadicRatio ^ (n + 1) •27    ((dyadicRatio ^ (n + 1))⁻¹ •28      (evalZero S.analysis x - S.operator (n + 1) (evalZero S.analysis x)))29  rw [smul_smul, mul_inv_cancel₀ (dyadicRatio_pow_ne_zero _), one_smul]3031theorem norm_intrinsic_operator_approx_le32    (T : IntervalL1 ℝ →L[ℝ] S.IntrinsicSpace) (n : ℕ) :33    ‖(S.operator (n + 1)).comp ((evalZero S.analysis).comp T) -34      (evalZero S.analysis).comp T‖ ≤ dyadicRatio ^ (n + 1) * ‖T‖ := by35  apply ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg (pow_nonneg dyadicRatio_nonneg _) (norm_nonneg T))36  intro f37  change ‖S.operator (n + 1) (evalZero S.analysis (T f)) - evalZero S.analysis (T f)‖ ≤ _38  rw [norm_sub_rev, intrinsic_defect_eq μ S n (T f), norm_smul,39    Real.norm_eq_abs, abs_of_nonneg (pow_nonneg dyadicRatio_nonneg _)]40  calc41    _ ≤ dyadicRatio ^ (n + 1) * ‖T f‖ := mul_le_mul_of_nonneg_left42      (norm_intrinsic_coord_le μ S (n + 1) (T f)) (pow_nonneg dyadicRatio_nonneg _)43    _ ≤ dyadicRatio ^ (n + 1) * (‖T‖ * ‖f‖) :=44      mul_le_mul_of_nonneg_left (T.le_opNorm f) (pow_nonneg dyadicRatio_nonneg _)45    _ = _ := (mul_assoc _ _ _).symm4647variable (hS : ∀ n (A : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ),48  DyadicVanishing ((S.operator n).comp A))4950include hS5152theorem dyadicVanishing_intrinsic_evalZero (T : IntervalL1 ℝ →L[ℝ] S.IntrinsicSpace) :53    DyadicVanishing ((evalZero S.analysis).comp T) := by54  apply dyadicVanishing_of_opNorm_tendsto _55    (fun n => (S.operator (n + 1)).comp ((evalZero S.analysis).comp T))56  · intro n57    exact hS (n + 1) _58  · apply squeeze_zero (fun n => norm_nonneg _) (norm_intrinsic_operator_approx_le μ S T)59    have hp : Tendsto (fun n : ℕ => dyadicRatio ^ (n + 1)) atTop (𝓝 0) := by60      simpa only [pow_succ, zero_mul] using61        (tendsto_pow_atTop_nhds_zero_of_lt_one dyadicRatio_nonneg dyadicRatio_lt_one).mul_const dyadicRatio62    simpa only [zero_mul] using hp.mul_const ‖T‖6364theorem dyadicVanishing_intrinsic_coord (T : IntervalL1 ℝ →L[ℝ] S.IntrinsicSpace) (n : ℕ) :65    DyadicVanishing ((coord S.analysis n).comp T) := by66  have hzero := dyadicVanishing_intrinsic_evalZero μ S hS T67  cases n with68  | zero => exact hzero69  | succ n =>70    have he : (coord S.analysis (n + 1)).comp T =71        (dyadicRatio ^ (n + 1))⁻¹ •72          ((evalZero S.analysis).comp T -73            (S.operator (n + 1)).comp ((evalZero S.analysis).comp T)) := by74      ext1 f75      rw [ContinuousLinearMap.comp_apply, coord_eq]76      rfl77    rw [he]78    exact (hzero.sub (hS (n + 1) _)).smul _7980variable [SFinite μ]8182theorem dyadicVanishing_intrinsic_flatten (T : IntervalL1 ℝ →L[ℝ] S.IntrinsicSpace) :83    DyadicVanishing ((IntervalModel.flattenIsometry (𝕜 := ℝ) μ).toContinuousLinearMap.comp84      (S.inclusion.toContinuousLinearMap.comp T)) := by85  apply dyadicVanishing_flatten_of_coordinates86  intro n87  exact dyadicVanishing_intrinsic_coord μ S hS T n8889theorem not_boundedBelow_intrinsic (T : IntervalL1 ℝ →L[ℝ] S.IntrinsicSpace)90    {c : ℝ} (hc : 0 < c) (hlower : ∀ f, c * ‖f‖ ≤ ‖T f‖) : False := by91  apply not_boundedBelow_sum_of_coordinates μ (S.inclusion.toContinuousLinearMap.comp T)92    (fun n => dyadicVanishing_intrinsic_coord μ S hS T n) hc93  intro f94  simpa only [ContinuousLinearMap.comp_apply, LinearIsometry.coe_toContinuousLinearMap,95    LinearIsometry.norm_map] using hlower f9697end PL1.EnfloBush98