OAI/Analysis/HenonEmden/Intervals.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral line 11

    Source documentation

    Integral over the segment of half-length r centered at x.

    noncomputable def segmentIntegral (k : ℝ → ℝ) (r x : ℝ) : ℝ :=
…
  2. lemma OAI.HenonLaneEmden.IntervalGeometry.primitive_hasDerivAt line 14
  3. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_eq_primitive line 19
  4. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_hasDerivAt line 27
  5. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_continuous line 37
  6. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_even line 41
  7. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_antitoneOn line 49
  8. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_abs line 62
  9. lemma OAI.HenonLaneEmden.IntervalGeometry.segmentIntegral_antitone_abs line 69
  10. lemma OAI.HenonLaneEmden.IntervalGeometry.integral_translate_eq_segment line 77
  11. lemma OAI.HenonLaneEmden.IntervalGeometry.midpoint_endpoint_sign line 86

    Source documentation

    The drift of the two interval midpoints has the opposite sign to the integrated endpoint difference of a symmetric decreasing kernel.

    lemma midpoint_endpoint_sign {k : ℝ → ℝ} (hk : Continuous k)
    (heven : ∀ x, k (-x) = k x)
    (hanti : ∀ {x y : ℝ}, |x| ≤ |y| → k y ≤ k x)
    {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) :
    ((a+b)/2-(c+d)/2) * (∫ y in c..d, (k (b-y)-k (a-y))) ≤ 0 := by
…
  12. def OAI.HenonLaneEmden.IntervalGeometry.kernel line 112

    Source documentation

    Restricted Newton kernel; c is its (positive) normalization.

    noncomputable def kernel (n : ℕ) (l c h : ℝ) : ℝ :=
…
  13. lemma OAI.HenonLaneEmden.IntervalGeometry.base_pos line 115
  14. lemma OAI.HenonLaneEmden.IntervalGeometry.kernel_nonneg line 118
  15. lemma OAI.HenonLaneEmden.IntervalGeometry.kernel_even line 123
  16. lemma OAI.HenonLaneEmden.IntervalGeometry.kernel_continuous line 126
  17. lemma OAI.HenonLaneEmden.IntervalGeometry.kernel_hasDerivAt line 132
  18. lemma OAI.HenonLaneEmden.IntervalGeometry.kernel_antitone_abs line 143
  19. def OAI.HenonLaneEmden.IntervalGeometry.boxIntegral line 155
  20. lemma OAI.HenonLaneEmden.IntervalGeometry.boxIntegral_congr line 158
  21. lemma OAI.HenonLaneEmden.IntervalGeometry.boxIntegral_add line 163
  22. lemma OAI.HenonLaneEmden.IntervalGeometry.boxIntegral_sub line 174
  23. lemma OAI.HenonLaneEmden.IntervalGeometry.boxIntegral_const_mul line 185
  24. lemma OAI.HenonLaneEmden.IntervalGeometry.boxIntegral_swap line 189
  25. lemma OAI.HenonLaneEmden.IntervalGeometry.boxIntegral_nonneg line 197
  26. lemma OAI.HenonLaneEmden.IntervalGeometry.endpoint_defect line 203
  27. lemma OAI.HenonLaneEmden.IntervalGeometry.endpoint_defect_right line 221
  28. lemma OAI.HenonLaneEmden.IntervalGeometry.box_endpoint_defect_left line 239
  29. lemma OAI.HenonLaneEmden.IntervalGeometry.box_endpoint_defect_right line 255
  30. lemma OAI.HenonLaneEmden.IntervalGeometry.box_midpoint_identity line 268
  31. lemma OAI.HenonLaneEmden.IntervalGeometry.box_integral_derivative line 289
  32. lemma OAI.HenonLaneEmden.IntervalGeometry.box_midpoint_sign line 304
  33. lemma OAI.HenonLaneEmden.IntervalGeometry.box_endpoint_comparison line 314

    Source documentation

    General interval comparison before substituting the Newton kernel.

    lemma box_endpoint_comparison {k k' : ℝ → ℝ} (hk : Continuous k) (hk' : Continuous k')
    (hderiv : ∀ x, HasDerivAt k (k' x) x)
    (heven : ∀ x, k (-x) = k x)
    (hanti : ∀ {x y : ℝ}, |x| ≤ |y| → k y ≤ k x)
    {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) :
    boxIntegral a b c d (fun x y => 2*k (x-y) - (k (a-y)+k (b-y))/2 -
      (k (x-c)+k (x-d))/2) ≤
      boxIntegral a b c d (fun x y => -(x-y)*k' (x-y)) := by
…

    Mentions: OAI.HenonLaneEmden.IntervalGeometry.boxIntegral

  34. lemma OAI.HenonLaneEmden.IntervalGeometry.kernel_derivative_continuous line 336
  35. lemma OAI.HenonLaneEmden.IntervalGeometry.newton_endpoint_comparison line 343

    Source documentation

    The two unweighted endpoint defects are controlled by the directional interaction.

    lemma newton_endpoint_comparison (n : ℕ) (hn : 3 ≤ n) {l C a b c d : ℝ}
    (hl : 0 < l) (hC : 0 ≤ C) (hab : a ≤ b) (hcd : c ≤ d) :
    boxIntegral a b c d (fun x y => 2*kernel n l C (x-y) -
      (kernel n l C (a-y)+kernel n l C (b-y))/2 -
      (kernel n l C (x-c)+kernel n l C (x-d))/2) ≤
      ((n : ℝ)-2)*boxIntegral a b c d
        (fun x y => (x-y)^2/(l^2+(x-y)^2)*kernel n l C (x-y)) := by
…

    Mentions: OAI.HenonLaneEmden.IntervalGeometry.boxIntegral, OAI.HenonLaneEmden.IntervalGeometry.kernel

  36. lemma OAI.HenonLaneEmden.IntervalGeometry.weighted_scalar_comparison line 361
  37. lemma OAI.HenonLaneEmden.IntervalGeometry.bounded_weighted_interval_comparison line 377

    Source documentation

    Weighted interval comparison, with finite endpoints. The normalizing constant C may be instantiated by 1 / ((n-2) * area(S^(n-1))).

    lemma bounded_weighted_interval_comparison (n : ℕ) (hn : 3 ≤ n)
    {l C a b c d cI cJ : ℝ} (hl : 0 < l) (hC : 0 ≤ C)
    (hab : a ≤ b) (hcd : c ≤ d) (hcI : 0 ≤ cI) (hcJ : 0 ≤ cJ) :
    (cI+cJ) * boxIntegral a b c d (fun x y => kernel n l C (x-y)) ≤
      cI * boxIntegral a b c d (fun _ y => (kernel n l C (a-y)+kernel n l C (b-y))/2) +
      cJ * boxIntegral a b c d (fun x _ => (kernel n l C (x-c)+kernel n l C (x-d))/2) +
      (((n : ℝ)-2)*min cI cJ) * boxIntegral a b c d
        (fun x y => (x-y)^2/(l^2+(x-y)^2)*kernel n l C (x-y)) +
      |cI-cJ| * boxIntegral a b c d (fun x y => kernel n l C (x-y)) := by
…

    Mentions: OAI.HenonLaneEmden.IntervalGeometry.boxIntegral, OAI.HenonLaneEmden.IntervalGeometry.kernel

  38. lemma OAI.HenonLaneEmden.IntervalGeometry.ofReal_boxIntegral line 404
  39. lemma OAI.HenonLaneEmden.IntervalGeometry.bounded_weighted_interval_lintegral line 425
  40. inductive OAI.HenonLaneEmden.IntervalGeometry.OpenInterval line 485

    Source documentation

    The four kinds of nonempty open real intervals. Valid excludes reversed finite endpoints; no endpoints at infinity are ever evaluated.

    inductive OpenInterval where
…
  41. def OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.carrier line 493
  42. def OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.Valid line 499
  43. def OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.IsBounded line 503
  44. def OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.leftAverage line 507
  45. def OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.rightAverage line 512
  46. lemma OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.leftAverage_nonneg line 517
  47. lemma OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.rightAverage_nonneg line 523
  48. lemma OAI.HenonLaneEmden.IntervalGeometry.OpenInterval.exists_bounded line 529
  49. lemma OAI.HenonLaneEmden.IntervalGeometry.weighted_interval_comparison line 538

    Source documentation

    The full interval comparison, including unbounded zero-weight intervals. All expressions are nonnegative extended integrals, so no divergent quantities are subtracted. The harmless zero continuation of the endpoint average is used only when the corresponding coefficient vanishes.

    lemma weighted_interval_comparison (n : ℕ) (hn : 3 ≤ n)
    (I J : OpenInterval) (hI : I.Valid) (hJ : J.Valid)
    {l C cI cJ : ℝ} (hl : 0 < l) (hC : 0 ≤ C) (hcI : 0 ≤ cI) (hcJ : 0 ≤ cJ)
    (hboundedI : 0 < cI → I.IsBounded) (hboundedJ : 0 < cJ → J.IsBounded) :
    (∫⁻ x in I.carrier, ∫⁻ y in J.carrier,
      ENNReal.ofReal ((cI+cJ)*kernel n l C (x-y))) ≤
    ∫⁻ x in I.carrier, ∫⁻ y in J.carrier,
      ENNReal.ofReal (cI*I.leftAverage (kernel n l C) y +
        cJ*J.rightAverage (kernel n l C) x +
        (((n:ℝ)-2)*min cI cJ*((x-y)^2/(l^2+(x-y)^2))+|cI-cJ|)*kernel n l C (x-y)) := by
…

    Mentions: OAI.HenonLaneEmden.IntervalGeometry.OpenInterval, OAI.HenonLaneEmden.IntervalGeometry.kernel