noncomputable def G67SumCoordinate.boxKernel (a b c d : ℝ) (φ : ℝ → ℝ) (x : ℝ × ℝ) : ℝ

Compactly supported original integrand, before the measure-preserving shear.

Equations

• G67SumCoordinate.boxKernel a b c d φ x = (Set.Icc a b ×ˢ Set.Icc c d).indicator (fun (x : ℝ × ℝ) => φ (x.1 + x.2) / (x.1 * x.2)) x

theorem G67SumCoordinate.boxKernel_integrable {a b c d : ℝ} {φ : ℝ → ℝ} (ha : 0 < a) (hc : 0 < c) (hφ : ContinuousOn φ (Set.Icc (a + c) (b + d))) : MeasureTheory.Integrable (boxKernel a b c d φ) (MeasureTheory.volume.prod MeasureTheory.volume)

The positive compact rectangle supplies the Fubini integrability hypothesis.

theorem G67SumCoordinate.integral_closed_indicator {a b : ℝ} (hab : a ≤ b) (f : ℝ → ℝ) : ∫ (x : ℝ), (Set.Icc a b).indicator f x = ∫ (x : ℝ) in a..b, f x

Conversion of a closed interval indicator to its oriented interval integral.

theorem G67SumCoordinate.integral_boxKernel {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (φ : ℝ → ℝ) : ∫ (u : ℝ) (v : ℝ), boxKernel a b c d φ (u, v) = ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, φ (u + v) / (u * v)

The indicator rectangle has precisely the original iterated integral.

theorem G67SumCoordinate.sheared_boxKernel (a b c d s u : ℝ) (φ : ℝ → ℝ) : boxKernel a b c d φ (u, s - u) = (Set.Icc (a + c) (b + d)).indicator (fun (s : ℝ) => (Set.Icc (lower a d s) (upper b c s)).indicator (fun (u : ℝ) => φ s / (u * (s - u))) u) s

Pointwise moving-domain identity. The outer sum indicator is essential.

theorem G67SumCoordinate.rectangle_sum_fibers {a b c d : ℝ} {φ : ℝ → ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc (a + c) (b + d))) : ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, φ (u + v) / (u * v) = ∫ (s : ℝ) in a + c..b + d, ∫ (u : ℝ) in lower a d s..upper b c s, φ s / (u * (s - u))

Pure sum-coordinate Fubini formula with the fiber still unevaluated.

theorem G67SumCoordinate.rectangle_sum_formula {a b c d : ℝ} {φ : ℝ → ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc (a + c) (b + d))) : ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, φ (u + v) / (u * v) = ∫ (s : ℝ) in a + c..b + d, φ s * weight a b c d s

Exact one-dimensional logarithmic formula; only positivity and continuity are inputs.