kernel_integral_match

formal source

 107  kernel_match_pointwise ϑ hϑ
 108
 109/-- The integrand match: ∫ J(r(ϑ)) dϑ = 2 ∫ tan ϑ dϑ -/
 110theorem kernel_integral_match (θ_s : ℝ) (hθ : 0 < θ_s ∧ θ_s < π/2) :
 111  ∫ ϑ in (0)..(π/2 - θ_s), Jcost (recognitionProfile (ϑ + θ_s)) =
 112  2 * ∫ ϑ in (0)..(π/2 - θ_s), Real.cot (ϑ + θ_s) := by
 113  -- Follows by integrating the pointwise identity
 114  -- measurability and integrability are standard for these smooth functions
 115  have hb_nonneg : 0 ≤ π/2 - θ_s := sub_nonneg.mpr (le_of_lt hθ.2)
 116  have hpt : ∀ ϑ ∈ Set.Icc (0 : ℝ) (π/2 - θ_s),
 117      Jcost (recognitionProfile (ϑ + θ_s)) = 2 * Real.cot (ϑ + θ_s) := by
 118    intro ϑ hϑ
 119    apply kernel_match_pointwise (ϑ + θ_s)
 120    constructor
 121    · have hθ_nonneg : 0 ≤ θ_s := le_of_lt hθ.1
 122      exact add_nonneg hϑ.1 hθ_nonneg
 123    · have : ϑ ≤ π/2 - θ_s := hϑ.2
 124      have hsum := add_le_add_right this θ_s
 125      simpa [add_comm, add_left_comm, add_assoc] using hsum
 126  have h_ae :
 127      ∀ᵐ ϑ ∂MeasureTheory.volume,
 128        ϑ ∈ Set.uIoc 0 (π/2 - θ_s) →
 129          Jcost (recognitionProfile (ϑ + θ_s)) = 2 * Real.cot (ϑ + θ_s) := by
 130    refine Filter.Eventually.of_forall ?_
 131    intro ϑ hϑ
 132    have hIoc : ϑ ∈ Set.Ioc (0 : ℝ) (π/2 - θ_s) := by
 133      simpa [Set.uIoc, hb_nonneg] using hϑ
 134    have hIcc : ϑ ∈ Set.Icc (0 : ℝ) (π/2 - θ_s) := by
 135      exact ⟨le_of_lt hIoc.1, hIoc.2⟩
 136    exact hpt ϑ hIcc
 137  have hcongr :=
 138    intervalIntegral.integral_congr_ae
 139      (μ := MeasureTheory.volume)
 140      (a := 0) (b := π/2 - θ_s)