theorem
proved
tactic proof
kernel_integral_match
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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)
141 (f := fun ϑ => Jcost (recognitionProfile (ϑ + θ_s)))
142 (g := fun ϑ => 2 * Real.cot (ϑ + θ_s)) h_ae
143 simpa using hcongr
144
145end Measurement
146end IndisputableMonolith